×

TICC-PARADIGM TO BUILD VERIFIED PARALLEL SOFTWARE FOR MULTI-CORE CHIPS

  • US 20090307660A1
  • Filed: 05/05/2009
  • Published: 12/10/2009
  • Est. Priority Date: 10/14/2008
  • Status: Active Grant
First Claim
Patent Images

1. TICC™

  • -Ppde, the integrated Parallel program development and execution platform, based on a modified version of TICC™

    , Technology for Integrated Computation and Communication, U.S. Pat. No. 7,210,145 B2, inventor Chitoor V. Srinivasan, teaches following methods;

    methods(1.1) for implementing parallel computer programs for applications, A;

    TICC™

    -Ppde providing methods for implementing parallel computer programs for an application A, starting from abstract specifications of interactions among abstract software computing units called cells, the set of cells together with all interaction specifications associated with them being the abstract design for parallel programs of application A, called A;

    DESIGN(), progressively refining cells and interactions in A;

    DESIGN() to their final fully refined implementation, defining design requirements at the time of design in a formal language called Causal Temporal Language, herein after referred to by CTL, parallel computer programs in application A at any stage of refinement being called A;

    implementation(), design requirements being updated by designers at every stage of refinement, design requirements at every stage of refinement being called A;

    requirements(), the set of all cells in A;

    implementation() being called A;

    cells(), each cell in A;

    cells() interacting with other cells in A;

    cells() only through message exchanges via already established communication pathways, each cell running in its own dedicated hardware CPU (hardware ComPuting Unit), this CPU not being shared with any other cell in A;

    cells() ;

    methods(1.2) for message exchanges unique to TICC™

    -Ppde;

    the difference between TICC™

    parallel programming paradigm and all other parallel programming paradigms being in the way TICC™

    -Ppde manages point-to-point and group-to-group communications among cells in A;

    cells(), enabling each cell itself to deliver messages it computes to their intended destination cells, immediately after a message becomes ready to be sent, in parallel with all other such message exchanges occurring simultaneously in A;

    implementation(), allowing almost instantaneous guaranteed asynchronous synchronized message deliveries to intended destinations with precisely predictable latencies of the order of at most a few hundreds of nanoseconds, assuming 2-gigahertz CPUs, with no need for message scheduling or synchronization sessions;

    methods(1.3) for formally verifying A;

    implementation();

    at each stage of refinement, including the A;

    DESIGN() stage, TICC™

    -Ppde automatically generating an event based model of computations up to that stage of refinement, this model being called ALLEOPs (ALLowed Event Occurrence Patterns), ALLEOPs for A;

    DESIGN() being called A;

    designALLEOPS() and ALLEOPs for A;

    implementation() at any stage of refinement being called A;

    ALLEOPS(), TICC™

    -Ppde using A;

    designALLEOPS() and A;

    ALLEOPS() to validate designs and implementations at any stage of refinement through formal verification of CTL statements in A;

    requirements(), TICC™

    -Ppde using A;

    designALLEOPS() and A;

    ALLEOPS() to find validity proofs for CTL-assertions in A;

    requirements(), interacting with users during search for proofs, users providing additional CTL-assertions to guide proof search where necessary;

    methods(1.4), for running fully refined A;

    implementation() with automatic self-monitoring using TICC™

    -Ppde SMS (Self-Monitoring System);

    A;

    ALLEOPS() also being used by TICC™

    -Ppde for automatic dynamic monitoring of a fully refined A;

    implementation() for correct operation while A is running, in parallel with application A, throughout its life time, with little or no interference with timings of computational events occurring in application A, identifying and reporting errors, pending errors, and occurrences of a priori defined alert event patterns, this dynamic monitoring being done automatically by SMS (Self-Monitoring System) built into the communication mechanisms of TICC™

    -Ppde;

    methods(1.5), for running arbitrarily scalable A;

    implementation() in massively parallel multi-computer hardware systems;

    running scalable A;

    implementation() at efficiencies in the range of 80% to 100% in arbitrarily large numbers of CPUs (hardware ComPuting Units), such CPUs being,(i) CPUs in any SMP (Shared-memory MultiProcessor) with 32 or more CPUs, the CPUs in SMP communicating with each other using software shared memory communication pathways (sm-pathways) of TICC™

    -Ppde installed in A;

    implementation(), or(ii) CPUs in any DMP (Distributed-Memory multiprocessor) whose computing nodes are SMPs, each with 32 or more CPUs, the SMPs in the DMP communicating with each other using hardware distributed-memory communication pathways (hereinafter referred to as dm-pathways) of TICC™

    -Ppde, dm-pathways being embedded in a local area net, called TICCNET™

    , or(iii) CPUs in any multi-core chip implemented as an SMP containing 32 or more CPUs, all CPUs in the chip sharing a common memory and communicating with each other through software sm-pathways (shared-memory pathways) installed in A;

    implementation(), or(iv) multi-core chips containing 256 or more CPUs, all sharing a collection of independent Shared Memory Modules, hereinafter referred to as SMMs, each SMM allowing anywhere from 2 to 16 CPUs to share the SMM simultaneously, sharing of SMMs by CPUs in the chip being organized in a manner that exploits the virtualMemory organization of TICC™

    -Ppde, this organization providing increased execution efficiencies and dramatically improving data and system security, while at the same time eliminating the need to use TICCNET™

    for communications among independent CPUs and using independent SMMs, or(v) CPUs in an SCG (SuperComputing Grid), each computing node of SCG being either an SMP or a DMP integrated in a single chip, SCG containing an arbitrary but fixed number of such SMPs and DMPs, SMPs and DMPs in SCG being interconnected by dm-pathways in a local area TICCNET™

    ;

    methods(1.6), for building scalable CPPSS;

    implementation() for real-time Cyber-Physical Parallel Software Systems with built-in SMS (Self-Monitoring System) using same methods of implementation through abstract design, successive refinements, requirements specifications and validation through formal verification at each stage of refinement, and automatic run-time self-monitoring using SMS;

    methods(1.7), for building scalable AHS;

    implementation() for Asynchronous Hardware Systems or embedded systems with built-in SMS (Self-Monitoring System), using same methods of implementation through abstract design, successive refinements, validation through formal verification at each stage of refinement, and automatic run-time self-monitoring using SMS;

View all claims
  • 0 Assignments
Timeline View
Assignment View
    ×
    ×