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

• Current Assignee: EDSS Incorporated
• Original Assignee: EDSS Incorporated
• Inventors: Srinivasan, Chitoor V.
• Granted Patent: US 7,979,844 B2
• Time in Patent Office: Days
• US Class Current: 717/114
• CPC Class Codes: G06F 8/314 Parallel programming languages G06F8/313 takes precedence

Abstract

This invention teaches a way of implementing formally verified massively parallel programs, which run efficiently in distributed and shared-memory multi-core chips. It allows programs to be developed from an initial abstract statement of interactions among parallel software components, called cells, and progressively refine them to their final implementation. At each stage of refinement a formal description of patterns of events in computations is derived automatically from implementations. This formal description is used for two purposes: One is to prove correctness, timings, progress, mutual exclusion, and freedom from deadlocks/livelocks, etc. The second is to automatically incorporate into each application a Self-Monitoring System (SMS) that constantly monitors the application in parallel, with no interference with its timings, to identify and report errors in performance, pending errors, and patterns of critical behavior. This invention also teaches a way of organizing shared-memory for multi-processors that minimizes memory interference, protects data and increases execution efficiency.

Claims

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;

2. Methods as recited in claim 1 further including following methods for specifying A:

DESIGN() and building A;

TICC™

-network;

methods(2.1), for specifying A;

DESIGN();

A;

DESIGN() being an abstract specification of the control-structure of parallel computations in A;

implementation(), A;

DESIGN() specifying implicitly all message synchronization and coordination in application A and causal chains of action and communication events that may occur in computations performed by A, A;

DESIGN() having five abstract software components, (i) A;

cells(), (ii) A;

pathways(), (iii) A;

TICC™

-network(), (iv) A;

TIPS() and (v) A;

CIPS(), these components being described below;

(i) A;

TICC™

-network() (hereinafter called the network) being a graph with nodes and branches, branches interconnecting the nodes, nodes of this graph being abstract cells in A;

implementation() and branches of this graph being abstract communication-Pathways (hereinafter called pathways) that interconnect software communication ports (hereinafter called ports) attached to cells in the network, the set of all cells in the network being called A;

cells(), the set of all ports in the network being called A;

ports(), the set of all pathways in the network being called A;

pathways(), each cell in A;

cells() being intended to run in parallel with all other cells in A;

cells(), each in its own assigned hardware CPU (ComPuting Unit), each cell in the network intended to perform computations by exchanging messages with other cells in the network through ports attached to the cell via pathways connected to those ports, there being no limit to the number of ports a cell may have (in practice the number of ports attached to a cell being limited to

     16) but no port being attached to more than one cell, some cells in the network receiving inputs from the environment that is external to application A, this environment itself being represented in the network by an environment cell,

(ii) A;

pathways;

pathways interconnecting software ports attached to different cells in the network, ports being used by cells to send and receive messages via pathways connected to them, each port being attached to only one unique cell, called the parent-cell of the port, thereby preventing contention for ports from cells in A;

cells(), each port being connected to exactly one pathway, thereby preventing message interference during parallel message deliveries, many ports being connected to the same pathway enabling group-to-group communications, each port connected to a pathway being attached to a distinct cell, a port-group being a group of one or more ports connected to the same pathway, no two ports attached to the same cell being in a port-group, no two distinct port-groups containing ports in common, pathway enabling group-to-group communication among port-groups connected to a pathway, it being possible for a port-group to send message to itself via a self-loop pathway connected to that port-group, in all such group-to-group message exchanges the message sending port-group always sending a coordinated joint message from parent-cells of ports in that port-group to the message receiving port-group, such joint messages from message sending port-group being always coordinated and simultaneously delivered in parallel to the message receiving port-group, such coordination and synchronization of message transfers in group-to-group communications being automatically done by agents embedded in pathways,

(iii) A;

TIPS();

interactions among cells being specified by abstract Thread Interaction Primitives, called TIPs, each TIP providing an abstract specification of how a cell senses message delivered to any one of its ports, how it processes delivered message and responds to it, it being possible for a TIP to spawn computations over other cells in A;

TICC™

-network(), gathering responses from those other cells before computing and sending back the response message, each port of each cell in A;

cells() having an abstract TIP defined for it, only ten different kinds of TIPs being necessary to implement any parallel program, five kinds of TIPs being called synchronous TIPs and other five kinds asynchronous TIPs, sensing of a message by a cell at any one of its ports always causing the cell to process and respond to that message without fail by executing the fully refined TIP defined at that port, spreading computations over several other cells in A;

TICC™

-network() if necessary, gathering responses from cells in A;

TICC™

-network() in order to compute the response message, every message delivered to every port of a cell being sensed by the cell without fail, every service request message received by a cell at any one of its ports being responded to by the cell without fail, computations performed by cells being thus driven by message receipts, the set of all abstract TIPs defined in A;

DESIGN() being called A;

TIPS(),

(iv) computations being performed by each cell C by cyclically executing TIPs defined at ports attached to C, TIPs defined at ports of C being called C;

TIPS(), cyclic computations performed by each cell being specified, again in an abstract form, by Cell Interaction Protocols, called CIPs, the CIP defined for a cell C being called C;

CIP(), and the set of all CIPs defined for cells in A;

DESIGN() being called A;

CIPS(),

all specifications up to this point being abstract, the abstract specifications merely identifying place-holders for methods and conditions used in A;

DESIGN(), A;

DESIGN() also implicitly specifying coordination and synchronization of message exchanges and computations performed by cells in A;

cells() and causal chains of action events and communication events that may occur in application A, while it is running

methods(2.3), structure of sm-pathways;

every sm-pathway (shared-memory pathway) S that delivers messages having a unique software memory component called virtualMemory M, embedded in S, the virtualMemory M embedded in sm-pathway S being called S.vM, no two distinct sm-pathways using the same virtualMemory, virtualMemories being declared during definition of sm-pathways, real memories being assigned to virtualMemories during compile or run time, S.vM holding messages delivered to ports in a port-group of one or more ports connected to S, S.vM also holding messages written by parent-cells of ports connected to S, in addition, S.vM holding computer program codes to process messages in S.vM and write new messages into S.vM by parent-cells of ports connected to S, each S.vM having software agents attached to it, no agent being attached to more than one virtualMemory, the set of all agents attached to S.vM being called S.agents, agents in S.agents being used by S to route, coordinate and synchronize message transfers via pathway S, to enforce message security, and to drive mechanisms that run the SMS (Self-Monitoring System) of TICC™

-Ppde, the mechanisms embedded in pathways for running SMS being the unique feature that distinguishes TICC™

-Ppde pathways from all other communication pathways used in all other computer programming systems, each port being connected to S by being connected one unique agent attached to S.vM, all ports connected to any one agent in S.agents constituting a port-group, pG, it being possible for a port-group to contain only one port, distinct ports in pG being attached to distinct cells, no two ports of the same cell being in any port-group, distinct port-groups being connected to distinct agents in S.agents, C.p being a port in pG attached to cell C, the pathway S connected to C.p being called C.p.pathway, C.p.pathway=S, and the virtualMemory of C.p.pathway being called C.p.vM, C.p.vM=S.vM=pG.vM, all ports in pG having the same virtualMemory associated with them, no two pathways being ever connected to the same port, no two ports C.p and C.q attached to the same cell being connected to the same pathway unless [C.p, C.q] belonged to a vector of ports called port-vector of the cell, every port C.p giving access to data and methods in pG.vM=C.p.vM only to its parent-cell C, no other cell in A;

cells() other than parent-cells of ports connected to a pathway S being able to access data and methods in S.vM, components in a pathway that exchange signals being always tuned to each other, such tuning enabling each component in the pathway to be always ready to receive and respond immediately to signals sent to it by other components in the pathway, thereby speeding up message transfers considerably, each port C.p being automatically tuned to the agent connected to it at the time the connection is established, agents attached to C.p.vM and exchanging signals also being tuned to each other at the same time, also at the time C.p is tuned to an agent attached C.p.vM both C.p and its parent-cell C being tuned to C.p.vM, these tunings happening automatically when a pathway is connected to its ports, union of S;

ports(), the set of all ports connected to S, S;

agents() the set of all agents in S and S.vM being called the components of pathway S, all components in sm-pathways being software components, no two sm-pathways ever sharing any components in common, thereby eliminating message interference during simultaneous parallel message transfers, FIGS. 2, 17, 19 and 23 showing examples of point-to-point, self-loop, group-to-group and ring-pathways, respectively, FIGS. 1 and 3 illustrating sm-pathways with no virtualMemories, such sm-pathways exchanging only signals and no messages, FIGS. 2, 4, 19 and 23 illustrating sm-pathways with virtualMemories, called Das-Pathways, TICC™

-Ppde providing methods for installing sm-pathways in A;

TICC™

-network() and modifying them;

methods(2.4), structure of dm-pathways;

the structure of a dm-pathway (distributed-memory pathway) D_i for 0≦

i<

N in TICCNET™

being illustrated in FIG. 24, D_i being connected to a generalPort port-group pG_i0 in an SMP, shown on the left of FIG. 24, the distributed computing network consisting of n SMPs, SMP[j] for 0≦

j<

n, the index j in SMP[j] being a function of the subscripts i and 0 in pG_i0 written as j=f(i,0), SMP[j] being thus written as SMP[f(i,0)], pathway D_i connecting the generalPort port-group pG_i0 in SMP[f(i,0)], to functionPort groups pF_ik 1≦

k<

m<

n, in other distinct SMPs, SMP[f(i,k)], of the same distributed computing network, f(i,k)≠

f(i,0), pG_i0.vM being the virtualMemory shared in common by all generalPorts in pG_i0, and similarly pF_ik.vM being the virtualMemory shared by all functionPorts in pF_ik, pG_i0.vM being in the SMP, SMP[f(i,0)=j], pF_ik.vM for 1≦

k<

m<

n being in the SMP, SMP[f(i,k)], the set of all (m+1) virtualMemories in the dm-pathway D_i being called D_i.vMs, D_i.vMs[0]=pG_i0.vM, D_i.vMs[k]=pF_ik.vM for 1≦

k<

m<

n, D_i.vMs={D_i.vMs[k]|0≦

k<

m}, there being two agents, a₀[i,k] and a₁[i,k] attached to each virtualMemory D_i.vMs[k], a₀[i,k] being a software agent and a₁[i,k] being a hardware agent, all ports in pG_i0 being connected and tuned to the software agent a₀[i,k], a₁[i,k] being connected to hardware signal and data lines of D_i as shown in said FIG. 24, the hardware signal and data lines thus interconnecting all agents a₁[i,k] for 0≦

j≦

m linking pathway segments [pG_i0a₀[i,0]a₁[i,0]] in SMP[f(i,0)] to the set of all pathway segments {[a₁[i,k]a₀[i,k]pG_ik]|1≦

k≦

m}, the segment [pG_i0a₀[i,0]a₁[i,0]] being called the message sending probe, the segments [[a₁[i,k]a₀[i,k]pG_ik]|1≦

k≦

m] being called message receiving probes, each SMP having multiple message sending and message receiving probes connecting it to the TICCNET™

, the resulting dm-pathway D_i being written as

D_i=[pG_i0a₀[i,0]a₁[i,0]{[a₁[i,k]a₀[i,k]pG_ik]|1≦

k≦

m},

port-group pG_i0 broadcasting message in parallel through the probe [pG_i0a₀[i,0]a₁[i,0]] and via hardware signal and data lines connected to a₁[i,0] to agents a₁[i,k] in the message receiving probes in the set {[a₁[i,k]a₀[i,k]pG_ik]|1≦

k<

m_i}, the message receiving probes delivering the message to every port-group pF_ik simultaneously, port-groups in {pF_ik|1≦

k<

m} sending back response messages in sequence one after the other in a multiplexed mode to pG_i0, no two dm-pathways sharing components in common, there being thousands of such distinct dm-pathways D_i, 0≦

i<

n>

1000 in a TICCNET™

, TICCNET™

providing mechanisms to dynamically install and dismantle such dm-pathways, each installed dm-pathway remaining in TICCNET™

until it is dismantled and a new pathway being installed, all dm-pathways in TICCNET™

together being capable of exchanging thousands of messages in parallel simultaneously without mutual interference, TICCNET™

providing guaranteed high-speed parallel message deliveries with latencies of the order of 500 nanoseconds plus signal transmission times, these being the unique features of TICCNET™

, TICC™

-Ppde providing methods for installing dm-pathways in A;

TICC™

-network(), dismantling installed pathways and/or modifying them, the set of all agents in application A in all its sm-pathways and dm-pathways being called A;

agents(), the set of all virtualMemories in application A being called A;

virtualMemories();

methods(2.5), structure of virtualMemories;

each virtualMemory, M, containing four components, (i) readMemory M.rd, (ii) writeMemory M.wr, (iii) executionMemory M.ex, and (iv) scratchPad M.sp, for a C.p.pathway with virtualMemory C.p.vM=M, C.p.rd=M.rd, C.p.wr=M.wr, C.p.ex=M.ex, C.p.scp=M.scp, C.p.rd being used by the parent cell C of C.p to read message delivered to C.p by C.p.pathway, C.p.wr being used by C to write new message and send it out via C.p.pathway, the read/write memories of M being switched before message delivery so that each message receiving cell always reads its delivered message from its readMemory, C.p.ex being used by C to run methods that process received messages in C.p.rd and C.p.wr, write message into C.p.wr, for any two distinct ports C_i.p and C_j.p in a port-group, pG, attached to distinct parent-cells C_i and C_j, C_i.p.vM=C_j.p.vM=pG.vM=M, M being the common virtualMemory of all ports in the port-group, C_i.p.sp=C_j.p.sp==pG.sp=M.sp being the common scratchPad memory used by parent-cells of ports in pG, M.sp being used by parent-cells C_i of all ports C_i.p in pG to exchange data with each other while processing in parallel messages in M, in order to coordinate their respective computations and send back a joint response, M providing execution environment for all computer program codes residing in M, TICC™

-Ppde providing methods for installing virtualMemories in pathways and modifying them;

methods(2.6), CCPs and protocols;

each port C.p in A;

ports() and each pathway C.p.pathway having a software protocol called C.p.protocol defined for it, each C.p.protocol containing concatenations of the special programming primitive unique to TICC™

-Ppde, called CCPs (Causal Communication Primitives), introduced in Section 1.1 of CHAPTER 3, each CCP having the form X;

x→

Y, X and Y being cells, or ports or agents in a pathway, x being a start or completion signal, concatenations of CCPs having the form X;

x→

Y;

y→

Z, X, Y and Z being all components in the same pathway and x, y being signals, it being possible for each type of signal to have subtypes defined for it, execution of CCPs in C.p.protocol causing components in C.p.pathway to exchange signals between each other, the signals so exchanged traveling over C.p.pathway eventually establishing a context, the said context causing the message in C.p.vM to be ultimately delivered to intended recipient ports also connected to the same C.p.pathway in the case of sm-pathways, the said context causing the message in C.p.vM to be transported to virtualMemories of intended recipient port-groups via hardware signal and data lines in the case of dm-pathways, the CCPs appearing in protocols being possibly embedded in other programming language statements as described in Section 1, FIGS. 3 and 4, and Section 7, statements (7.1) through (7.4) of CHAPTER 3, none of the protocols in TICC™

-Ppde containing data-declarations and all of them containing CCPs, C.p.protocol being invoked and executed only by the parent cell C of port C.p, TICC™

-Ppde providing prepackaged and compiled protocols for exchanging messages via all kinds of pathways likely to be used in any TICC™

-Ppde parallel program, implementers having the responsibility to define only unusual protocols that may be needed in application A, in a manner that is consistent with the protocol definition formats used in TICC™

-Ppde, TICC™

-Ppde providing methods for defining protocols using CCPs;

methods(2.7), for tuning components in a pathway;

components in C.p.pathway, connected to any port C.p of cell C exchanging signals to transport and deliver message in the virtualMemory C.p.vM to its intended recipients, components in C.p.pathway being always tuned to each other, tuning causing components in C.p.pathway to be always ready to receive and immediately respond to signals sent by other components in C.p.pathway, tuning eliminating need for synchronization sessions during signal exchanges thereby speeding up message exchanges considerably, tuning a port C.p to components in C.p.pathway being accomplished automatically in TICC™

-Ppde at the time C.p.pathway is connected to C.p, tuning C.p to components in C.p.pathway causing parent cell of C.p also to be tuned to the unique virtualMemory C.p.vM of C.p.pathway, there being no need for implementers of application A to tune components in a pathway, or to schedule or synchronize signal exchanges, scheduling message exchanges via pathways being done automatically during TIP executions, scheduling signal exchanges among pathway components being automatically done by CCPs in protocols, coordinating message dispatch and synchronizing message deliveries being done by agents on pathways, agents in a pathway also managing signal exchange mechanisms for driving the SMS of TICC™

-Ppde during message transmissions and enforcing message security, as described in Section 7 of CHAPTER 3, all tuning, coordination, synchronization and support for driving SMS being built-in features of all TICC™

-Ppde protocols, all of these capabilities being automatically enabled by TICC™

-Ppde when pathways are installed and connected to their respective ports in A;

implementation(), implementers having nothing to do to implement, or invoke and execute any of these features of any installed pathway in any application, TICC™

-Ppde providing methods for installing pathway components in abstract pathways and tuning the components to each other;

methods(2.8), for data protection and parallel buffering;

each port C.p in a port-group allowing its parent cell C to access and use its virtualMemory C.p.vM, if and only if the said parent cell has either just sensed a message delivered to port C.p, or sensed readiness of port C.p to send out a message, multiple ports in a port-vector, C.p=[C.p₁, C.p₂, . . . , C.p_n] attached to the same parent cell giving simultaneous access to the parent cell C to all virtualMemories C.p_i.vM for 1≦

i<

≦

n when necessary, ports thus allowing their respective parent cells to access virtualMemories only when needed, it being never possible for parent cells of message sending ports and parent cells of message receiving ports connected to a pathway to both use the virtualMemory of that pathway simultaneously, it also being never possible for any parent cell of any port not connected to a pathway to access the virtualMemory of that pathway, thereby protecting data in virtualMemories from unauthorized access and use, thereby also preventing mutilation of data in virtualMemories and preserving the data in every virtualMemory until the said data are used by their intended users, thus the virtualMemories in A;

implementation() providing protected parallel buffering, supporting all asynchronous parallel communications in A;

implementation(), it being possible to design independent hardware Shared-Memory Modules, called SMMs, in the size range of 10 megabytes to a few gigabytes and dynamically assign the SMMs to virtualMemories during compile or run time, dynamically connecting the CPU that runs a cell to SMMs only when ports of the cell give access to their parent cells to virtualMemories associated with those SMMs, such memory organization providing intrinsic security, privacy and protection to all data and software in an application, privacy and protection being thus built into a system at its lower most level, TICC™

-Ppde thus providing methods for automatic data protection in any application, application programming having nothing to do in order to benefit from these built-in protection mechanisms;

methods(2.9), guaranteed high-speed parallel communications;

CCPs implemented in software taking 25 to 50 nanoseconds to execute in a 2-gigabertz CPU, it being possible to implement CCP as a machine instruction in a CPU, CCP implemented as a machine instruction taking only about 5 nanoseconds to execute in a 2-gigahertz CPU, point-to-point communications via sm-pathways requiring at most only six CCP executions (including agents that drive the SMS and enforce data security), group-to-group communications via sm-pathways taking up to 14 or more CCP executions depending on the number of ports in each port-group, group-to-group communications via dm-pathways requiring 30 or more CCP executions depending on the number of port-groups connected to the dm-pathways, no protocol execution ever invoking any data, program, process or thread not already defined in that protocol itself, such protocol executions changing only data already defined in the pathway of that protocol and nothing else, it thus being true that no operating system or any other monitoring system may schedule, synchronize or execute any part of any protocol, no protocol execution being ever interrupted while it is being executed, the entire protocol, C.p.protocol at each port C.p in A;

ports() being executed uninterrupted only by the parent cell C of C.p as soon as C completes writing into C.p.vM the message to be sent out, such automatic immediate scheduling of message transmissions, mutual tuning of components in pathways that exchange signals and elimination of need for sequential buffering in asynchronous communications, enabling very high speed guaranteed instantaneous asynchronous communications with latencies of the order of at most a few hundred nanoseconds, when protocols are executed by 2 gigahertz CPUs and CCPs are implemented as machine instructions, both sm-pathways and dm-pathways enabling simultaneous asynchronous parallel message transfers, the numbers of such asynchronous parallel message transfers occurring simultaneously in an application being limited only by the numbers of distinct pathways installed in that application, these numbers being in the range of tens of thousands or more, TICC™

-Ppde thus providing methods for guaranteed automatic high-speed parallel communications;

methods(2.10), automatic coordination of group-to-group message exchanges with one or more ports in each port-group;

ports C_i.p for 0≦

i<

n>

0 in a port-group pG being connected to distinct ports D_j.q in another port-group qG, 0≦

j<

m>

0 by a common group-to-group pathway, pG.pathway=qG.pathway, either the set of all parent cells, D_j, of ports in qG being distinct from the set of all parent cells, C_i, of ports in pG, or pG≡

qG being true, each C_i.p.pathway for i, 0≦

i<

n being a part of pG.pathway and each D_j.q.pathway for j, 0≦

j<

m being a part of qG.pathway≡

pG.pathway, these pathways being similar to diagrams shown in FIG. 19 or 17 of CHAPTER 3, or the diagram in FIG. 24, parent cells C_i of ports C_i.p in port-group pG executing asynchronously and in parallel the protocols C_i.p.protocol in order to send out a joint service request message, m, via pG.pathway to the ports D_j.q in qG, simultaneous asynchronous parallel executions of C_i.p.protocol by parent cells C_i over the same group-to-group pG.pathway being automatically coordinated by agents in pG.pathway, the said agents guaranteeing simultaneous synchronous parallel delivery of the joint service request message m from ports in pG to every port in qG exactly once, the said agents delivering a message to a port only if that port satisfies an a priori defined security condition for that message, the said agents also sending signals to SMS (Self-Monitoring System) activating the SMS to install message dispatch and message delivery events in SMS for the message being transmitted via pG.pathway, the group-to-group protocols C_i.p.protocol locking the port C_i.p immediately after C_i.p sends out message m, thereby preventing every C_i.p in pG from sending out a second service request message, each C_i.p in pG being allowed to send a second service request message only after that C₁.p has received from all D_j.q in qG a joint response message, m′

, to the service request message, m, it being further required, each C_i sense the receipt of m′

at C_i.p before C_i can send out a second service request message, m′

being always sent back by D_j.q in qG via the same group-to-group pathway, qG.pathway≡

pG.pathway, through which each D_j.q received the service request message m, TICC™

-Ppde thus providing methods for automatic coordination and synchronization of group-to-group message exchanges;

methods(2.11), uniqueness of TICC™

-Ppde pathways;

TICC™

-Ppde providing methods for the following six pathway capabilities;

(i) all pathways being able to simultaneously transport and deliver messages in parallel with each other without mutual interference,

(ii) all pathways containing built-in infrastructure to drive SMS (Self-Monitoring System) of TICC™

-Ppde and enforce data security,

(iii) all pathways transmitting messages asynchronously as soon as messages are ready with no need for message scheduling or synchronization sessions during message transmission,

(iv) all software or hardware components that exchange signals in each pathway being always tuned to each other, tuning enabling every component to be always ready to receive and immediately respond to signals received from other components in that pathway, thereby significantly speeding up message deliveries,

(v) every pathway sending a coordinated joint message from parent-cells of ports in one port-group and synchronously delivering in parallel that joint message to ports either in the same port-group or to ports in another port-group also connected to the same pathway,

(vi) every pathway providing guaranteed high-speed synchronized message deliveries to ports in a port-group with latencies of the order of a few hundred nanoseconds or less with precisely predictable bounds on those latencies, assuming 2-gigahertz CPUs,

these six capabilities of TICC™

-Ppde pathways together making TICC™

-Ppde pathways unique and different from communication pathways used in all other computer communication systems, including pathways used in TICC™

, TICC™

-Ppde providing methods to install and use pathways with the above unique characteristics;

methods(2.12), for defining A;

cells();

methods for defining a collection of software computing units called cells, A;

cells() being the set of all cells in application A, each cell being an instance of a class of cells, the class of cells being a subclass, hereinafter called Cell-Subclass, of the top level abstract TICC™

-Ppde class, called Cell, each cell in A;

cells() running in parallel with all other cells in A;

cells(), each cell running in a designated distinct CPU (ComPuting Unit) unique to that cell, no two cells sharing the same CPU, TICC™

-Ppde managing all CPU assignments to cells and activations of cells to run in their respective assigned CPUs, cells and communication pathways being specifically designed to efficiently run in arbitrarily large numbers of CPUs in a diversity of multi-core chips, cells also being specifically designed to run time critical Cyber Physical Parallel Software Systems in a diversity of multi-core chips, the design, verification and self-monitoring methodologies of TICC™

-Ppde being also used to design, verify and run asynchronous hardware components in any Asynchronous Hardware Systems, TICC™

-Ppde cells being particular specializations of TICC™

cells, it being the responsibility of implementers to define all TICC™

-Ppde cell subclasses (hereinafter referred to as Cell-Subclasses) needed for application A in a manner that is consistent with Cell-Subclass definition formats in TICC™

-Ppde, TICC™

-Ppde providing methods to define Cell-Subclasses and install cell instances in A;

TICC™

-networks();

methods(2.8), for defining A;

ports();

software ports being attached to cells in A;

cells(), cells in A;

cells() using the ports attached to them to send/receive messages, each port being an instance of a class of ports, the class of ports being a subclass, hereinafter called Port-Subclass, of the top level abstract port class of TICC™

-Ppde called Port, each port being attached to only one cell C in A;

cells(), C.p being any port p attached to cell C, A;

ports() being the set of all ports attached to cells in A;

cells(), C;

ports() being the set of ports attached to cell C, each C;

ports() for each C in A;

cells() having at least one generalPort called C.g, at least one functionPort called C.f, and at least one interruptPort called C.i, each C.g being an instance of the subclass of Port called GeneralPort, C.g being used by C to send out service request messages and receive back responses, each C.f being an instance of the subclass of Port called FunctionPort, C.f being used by C to receive and respond to service request messages, each C.i being an instance of the subclass of Port called InterruptPort, InterruptPort itself being a subclass of FunctionPort, interruptPort C.i being used by C to receive and respond to interrupt messages received from other cells in A;

cells(), it being never possible for any process not run by cells in A;

cells() to interrupt activities of any cell, TICC™

-Ppde containing definitions of all Port-Subclasses likely to be used in any TICC™

-Ppde parallel program, each port being an instance of a Port-Subclass, TICC™

-Ppde providing methods to define Port-Subclasses, install port instances and attach the port instances to cells, it being the responsibility of implementers to define only special Port-Subclasses that are specific to application A and not already defined in TICC™

-Ppde, in a manner that is consistent with Port-Subclass definition formats in TICC™

-Ppde;

methods(2.9), for defining A;

agents();

methods for defining software agents, agents being attached to virtualMemories of pathways in A;

pathways(), each agent being an instance of a class of agents, the class of agents being a subclass, called Agent-Subclass, of the top level abstract agent class of TICC™

-Ppde, called Agent, each agent being attached to only one virtualMemory called parent virtualMemory of the agent, thus preventing contention for agents from pathways in A;

pathways(), A;

agents() being the set of all agents attached to virtualMemories in A;

pathways(), TICC™

-Ppde containing definitions of all Agent-Subclasses likely to be used in TICC™

-Ppde parallel programs, each agent being an instance of an Agent-Subclass, TICC™

-Ppde providing methods to define Agent-Subclasses, install agent instances and attach agents to virtualMemories, it being the responsibility of implementers to define only special Agent-Subclasses that are specific to application A and not already defined in TICC™

-Ppde, in a manner that is consistent with Agent-Subclass definition formats in TICC™

-Ppde;

methods(2.10), for defining A;

virtualMemories();

methods for defining software objects called virtualMemories, each virtualMemory being an instance of a class of virtualMemories, the class of virtualMemories being a subclass, called VirtualMemory-Subclass, of the top level abstract virtualMemory class of TICC™

-Ppde, called VirtualMemory, each instance of virtualMemory being uniquely associated with only one sm-pathway, called parent pathway of the virtualMemory, thus preventing contention for virtualMemories from sm-pathways in A;

pathways(), each dm-pathway interconnecting a group of SMPs in a distributed computing system, each such dm-pathway containing as many virtualMemories as there are SMPs connected to that dm-pathway, A;

virtualMemories() being the set of all virtualMemories embedded in pathways of A;

pathways(), TICC™

-Ppde containing definitions of all VirtualMemory-Subclasses likely to be used in TICC™

-Ppde parallel programs, TICC™

-Ppde providing methods to define VirtualMemory-Subclasses, install virtualMemory instances in pathways, and dynamically assign hardware memories to virtualMemories, it being the responsibility of implementers to define only special VirtualMemory-Subclasses that are specific to application A and not already defined in TICC™

-Ppde, in a manner that is consistent with VirtualMemory-Subclass definition formats in TICC™

-Ppde;

methods(2.11), for defining A;

pathways();

each pathway being an instance of a class of pathways, the class of pathways being a subclass, hereinafter called Pathway-Subclass, of the top level TICC™

-Ppde abstract class called Pathway, pathways in shared-memory environments containing only software components, such shared-memory pathways being called sm-pathways, pathways in distributed-memory environments containing both software and hardware components, such distributed-memory pathways being called dm-pathways, the term pathway being used to refer to both sm-pathway and dm-pathway, the set of all pathways in application A being called A;

pathways(), TICC™

-Ppde providing definitions of all Pathway-subclasses for pathways likely to be used in parallel programming, each pathway being an instance of a Pathway-subclass, TICC™

-Ppde providing methods to define Pathway-subclasses, install pathway instances of and connect pathway instances to ports attached to cells in A;

TICC™

-network(), implementers having to define only Pathway-Subclasses that are specific to given applications and not already defined in TICC™

-Ppde, implementers being required to define all needed new Pathway-Subclasses as per rules of Pathway-Subclass definitions in TICC™

-Ppde;

methods(2.12), for defining A;

TICC™

-Network();

TICC™

-Ppde providing methods to install cell instances of abstract or fully refined definitions of Cell-Subclasses in A;

DESIGN(), cell instances so installed belonging to A;

cells(), methods for installing instances of abstract or fully refined definitions Port-Subclasses, and attaching port instances to cell instances in A;

cells(), the set of all port instances attached to cells in A;

cells() being called A;

ports(), methods for installing instances of abstract or fully refined specifications of Pathway-Subclasses and connecting them to ports in A;

ports(), the set of all such pathway instances installed in a design of an application A being called A;

pathways(), each sm-pathway S in A;

pathways() that transmits messages having a unique instance of virtualMemory, called S.vM, S.vM being the virtualMemory embedded in S, each dm-pathway D containing one virtualMemory in each SMP connected to that dm-pathway, the number of virtualMemories embedded in D being equal to the number of SMPs connected to D, D.vMs being the set of all virtualMemories embedded in the dm-pathway D, each virtualMemory in each pathway having attached to them unique agent instances of abstract or fully refined Agent-subclasses, the set of all such agent instances attached to virtualMemories of pathways in A;

pathways() being called A;

agents(), pathways in A;

pathways() interconnecting ports attached to cells in A;

cells(), each port being connected to exactly one agent in exactly one pathway, components of any sm-pathway S in A;

pathways() being S;

ports(), S;

agents() and S.vM, components of any dm-pathway D in A;

pathways() being D;

ports(), D;

agents() and D.vMs, no two distinct pathways sharing components in common, thereby preventing message interference during parallel message exchanges, A;

TICC-network() (hereinafter called the network) being the graph whose nodes are cells in A;

cells(), and whose branches are pathways in A;

pathways() that interconnect ports attached to cells, TICC™

-Ppde providing methods to define A;

TICC™

-Network();

methods(2.13), for building A;

TICC™

-Network();

one or more distinguished cells of a Cell-Subclass called Configurator (or Environment) being defined for application A, A;

DESIGN() containing at least one instance of Configurator called configurator (or environment) in each SMP, the configurator having been programmed to install, on cue from a user of application A, a starting sub-network of already defined A;

TICC-network() in each SMP sufficient to start application A running in CPUs assigned to cells in the starting sub-networks, the cells in the starting sub-network in each SMP having been programmed to install in parallel, using their respective initialization routines, the parts of A;

TICC-network() belonging to that SMP, TICC™

-Ppde providing methods to install all needed instances of abstract or fully refined subclasses of cells, ports, agents, virtualMemories and pathways in the network, methods to connect, attach and tune them to each other satisfying all TICC™

-Ppde connectivity rules, it being the responsibility of implementers to program the initialization routines defined in cell subclasses suitably so that the network is correctly built once application A is started with the said starting sub-network in each SMP, it also being the responsibility of implementers to develop computer programs for the initialization routines in a manner that prevents deadlocks from occurring during parallel network construction in each SMP, parallel building of the network being automatically coordinated by TICC™

-Ppde, TICC™

-Ppde providing methods to build already defined A;

TICC™

-Network();

methods(2.14), for displaying A;

TICC™

-network();

TICC™

-GUI (Graphical User Interface) being used to display A;

TICC-network() on a display screen, each SMP having its own dedicated display screen, opening the TICC™

-GUI screen for application A causing TICC™

-GUI to display on the display screen of each SMP an image of the configurator for application A, user clicking on the displayed image of configurator and selecting install option from a displayed menu causing the configurator in that SMP to install all cells and pathways in a starting subnet of A;

TICC-network() sufficient to start running the initialization routines of cells in the starting subnet of that SMP, each cell in the starting subnet running in a CPU of said SMP assigned to it by TICC™

-Ppde, cells in the starting subnet installing other cells and other pathways in A;

TICC-network(), each newly installed cell automatically getting activated by TICC™

-Ppde to run in an assigned CPU of said SMP, each such newly installed cell executing its own initialization routine to install yet other cells and pathways in the network in said SMP, the network thus growing in parallel until the entire network is built in all SMPs, it being the responsibility of implementers to define the initialization routines in a manner avoiding conflicts and deadlocks so that required network is correctly built, TICC™

-GUI displaying the installed network in each SMP or parts of the network anchored on cells specified by a user, examples of such network images for small applications in a single SMP being illustrated throughout the CHAPTER 3, TICC™

-GUI being a built-in subsystem of TICC™

-Ppde, TICC™

-Ppde providing methods to display any part of an installed A;

TICC™

-Network() in any application, A;

methods(2.15), for defining A;

messages();

messages being held by virtualMemories of pathways in A;

pathways(), each message being an instance of a class of message, the class of messages being a Msg-subclass, called Msg, of the top level abstract message class of TICC™

-Ppde, called Message, Msg referring to any Msg-subclass of Message, each Msg definition specifying message formats and data formats that may appear in message instances, m, of Msg, each Msg definition also specifying Msg-methods for processing messages and creating new message instances of Msg, pathways in A;

pathways() delivering instances of Msg-subclasses to ports C.p attached to cells C in A;

cells(), the set of all Msg-subclases defined for application A being called A;

messages(), it being the responsibility of implementers to define all Msg-subclases needed for application A, in a manner that is consistent with message subclass definition formats in TICC™

-Ppde, TICC™

-Ppde providing methods for defining A;

messages() ;

methods(2.16), defining Msg-methods;

virtualMemory M embedded in C.p.pathway of a port C.p attached to a cell C in A;

cells() being C.p.vM, the readMemory of C.p.vM being C.p.rd, C.p.wr being the writeMemory, C.p.rd holding a message instance m of a Msg-subclass Msg, the phrase C.p;

msg() referring to this message instance m, C.p.wr holding a message instance m′

of possibly another Msg-subclass Msg′

, C.p.wr;

msg() referring to this message instance m′

, the CPU that runs parent cell C of C.p executing Msg-methods defined in the Msg-subclasses Msg and Msg′

, the executionMemory C.p.ex providing execution environment to each Msg-method defined in the Msg-subclasses, Msg and Msg′

Msg-methods and Msg′

-methods defined in Msg-subclasses, Msg and Msg′

, respectively, having the formats Msg;

<

method-name>

(<

ports>

) and Msg′

;

<

method-name′

>

(<

ports′

>

), all ports C.q appearing in the argument <

ports>

, and all <

ports′

>

being attached to the parent cell C of port C.p, CPU running cell C using C.p;

<

method-name>

(<

ports>

) and C.p;

<

method-name′

>

(<

ports′

>

), respectively, to invoke and execute the respective methods in C.p.vM, these methods using data and other methods defined only in the following components associated with cell C, port C.p and other ports C.q appearing in <

ports>

or <

ports′

>

, the components being, (i) cell C, (ii) port C.p, (iii) messages C.p;

msg() and C.p.wr;

msg(), (iv) ports C.q appearing in the argument <

ports>

or <

ports′

> and

(v) messages C.q;

msg() and C.q.wr;

msg() residing in virtualMemories C.q.vM, any cell C executing any method defined in any Msg-subclass or in a Cell-subclass of C being able to use only data and other methods defined in other software components in pathways connected to ports of C, such pathways being always connected to ports of C, tuning and attachment being symmetric relations, these features isolating each cell C from all other cells in A;

cells(), parent-cells of message sending and message receiving ports connected to a pathway never using the virtualMemory of that pathway simultaneously, TICC™

-Ppde providing methods for defining Msg-methods as per rules given above;

methods(2.17), for defining A;

pthreads();

Msg-methods, Msg;

<

method-name>

(<

ports>

), defined in any Msg-subclass, Msg, or similarly defined cell methods, C;

<

method-name>

(<

ports>

), defined in any Cell-subclass, being called pthreads (parallel threads) since such methods are likely to be short sequential computer programs taking no more than 10 to 100 microseconds to complete execution in a 2 gigahertz CPU, pthreads being executed in parallel by cells in A;

cells(), the set of all such pthreads defined for application A being called A;

pthreads(), each pthread in A;

pthreads() being independent of all other pthreads in A;

pthreads() excepting pthreads executed in parallel by parent-cells of ports in a port-group in their common virtualMemory, M, and using M.sp to exchange data during parallel execution of the said pthreads in order to coordinate their, respective, parallel computations, TIPs isolating pthreads from all communications among cells, it being the responsibility of implementers to fully refine all abstract software units in A;

implementation() including pthreads and Msg-subclasses, update A;

requirements() during refinement, formal validation of A;

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

implementation(), TICC™

-Ppde providing methods for defining refinements for pthreads as per rules given above.

3. Methods as recited in claims 1 or 2 further including methods for implementing A:

DESIGN() through successive refinements to produce fully refined A;

implementation();

methods(3.1), for defining programming abstractions called TIPs (Thread Interaction Protocols);

TICC™

-Ppde provides methods for defining abstract specifications of interactions among cells in A;

cells() using TIPs, each TIP being defined at a port C.p of cell C, TIP defined at port C.p being called C.p;

TIP(), there being a C.p;

TIP() defined at each port attached to each cell C in A;

cells(), the set of all TIPs defined for a cell C being called C;

TIPS(), the set of all TIPs defined for application A being called A;

TIPS(), C.p;

TIP() specifying abstractly how cell C receives message at its port C.p, processes the received message and responds to it, or cell C builds a message and sends it out via port C.p, interactions among cells in A;

cells() occurring only through messages exchanged via pathways in A;

TICC-network(), the essential difference between TICC™

-Ppde and other similar systems based on message exchanges being in the way TICC™

-Ppde manages communications, each cell in TICC™

-Ppde itself delivering all messages with no need for message scheduling and synchronization sessions, guaranteeing very high speed instantaneous asynchronous parallel message deliveries with precisely predictable latencies in the range of at most a few hundred nanoseconds using 2 Gigahertz CPUs, only five different kinds of TIPs being necessary to cover the needs of all parallel programming, five kinds of TIPs called synchronous TIPs and five kinds called asynchronous TIPs, simple TIPs have the forms,

Synchronous TIP;

C.p;

TIP()=C.p;

<

guard>

?(){C.p;

tip()} 

 

(C.1)

Asynchronous TIP;

C.p;

TIP()=C.p<

guard>

?()*{C.p;

tip()} 

 

(C.2)

where C evaluates the synchronous guard C.p;

<

guard>

?() in (C.1) to check whether port C.p has a message delivered to it, executes C.p;

tip() if C.p has a message delivered to it, else C skips port C.p polls its next port, when C evaluates the asynchronous guard C.p<

guard>

?()* in (C.2) it waits at port C.p until a message is delivered to C.p, executes C.p;

tip() when message is delivered and then only polls its next port, C.p being connected to exactly one agent attached to the virtualMemory C.p.vM of C.p.pathway, C.p;

tip() being called the TIP-body, execution of C.p;

guard?() or C.p;

guard?()* at port C.p being called polling of C.p by cell C, the order in which cell C polls its ports being called the polling-cycle of C, the various kinds of TIPs needed to define any parallel program in TICC™

-Ppde being described in Chapter 3, examples using various kinds of TIPs appearing throughout Chapter 3, it being the responsibility of implementers to define C.p;

TIP() for each port in A;

ports() in a manner that is consistent with TIP definition formats in TICC™

-Ppde and intended design requirements of application A, TICC™

-Ppde providing methods for defining TIPs;

methods(3.2), Asynchronous guards;

C.p;

guard?() in statement (C.1) being an asynchronous guard having one of the forms C.p;

mR?() (‘

mR’

for ‘

messageReady’

) and C.p;

pR?() (‘

pR’

for ‘

pathwayReady’

), asynchronous guard being a condition implemented as a built-in computer program provided by TICC™

-Ppde, available for use in any implementation, implementers being free to define their own guards specific to given applications, A, not already defined in TICC™

-Ppde, guards being always based on signals or subtypes of signals exchanged by ports in application A, asynchronous guards being used by cell C in A;

cells() to poll its ports C.p to check whether C.p has a message delivered to it, or whether C.p is ready to send out a message, the guards returning truth values true or false the TIP-body C.p;

tip() in statement (C.1) being executed only if the guard returns truth value true, the TIP-body being skipped if the guard returns false, TIPs with asynchronous guards being called asynchronous TIPs, TICC™

-Ppde providing methods for defining asynchronous guards;

methods(3.3), Synchronous guards;

C.p;

guard?()* in statement (C.2) being a synchronous guard, the parent cell C executing the TIP-body only if C.p;

guard?()* returns true, else waiting at port C.p, repeatedly executing C.p;

guard?() until C.p;

guard?()* returns truth value true, executing the TIP-body in statement (C.2) when C.p;

guard?()* becomes true, then only proceeding to poll its next port, the symbol ‘

*’

appearing in the synchronous guard indicating to TICC™

-Ppde the need for this kind of repeated execution of the computer program implementing the guard until the guard returns true, TIPs with synchronous guards being called synchronous TIPs, TICC™

-Ppde providing methods for defining synchronous guards;

methods(3.4), for simple TIP execution at a functionPort;

assuming C.p in (C.1) refers to a functionPort C.f attached to cell C, C being the unique parent cell of C.f, C being the only cell that may use C.f, C.f receiving a joint service request message, m, from one or more other ports C′

.q, the message m received by C.f being stored in the readMemory C.f.rd of the virtualMemory C.f.vM≡

M, the virtualMemory M being embedded in C.f.pathway, phrase C.f;

msg() denoting the message in C.f.rd, the message C.f;

msg() delivered to C.f being sensed by cell C through evaluation of the guard C.p;

<

guard>

?()=C.f;

mR?() (′

mR?()′

for ‘

message Ready?’

) appearing in (C.1), evaluation returning truth value true causing cell C to respond to C.f;

msg() by executing the TIP-body C.p;

tip()=C.f;

r().s();

appearing in statement (C.2), C.f;

r() (‘

r’

for ‘

respond’

) being the abstraction of a pthread (parallel thread) used by C to process the service request message C.f;

msg() and write the response message in the writeMemory, C.f.wr of C.f.vM, the executionMemory, C.f.ex, of C.f.vM providing execution environment for the evaluation of this TIP-body C.p;

tip(), implementers being free to use any name for the pthread ‘

r()’

in C.f;

tip(), name used by implementers capturing the design intent for r(), parent cell C of C.f evaluating C.f;

s() immediately after evaluating C.f;

r() to invoke and execute eval(C.f.protocol) in order to transmit the response message written in C.f.wr immediately to ports C′

.q from which C.f received its service request message, execution of this protocol causing the read/write memories of C.f.vM to be switched before message delivery so that each C′

.q receives the response message written in C.f.wr in the readMemory C′

.q.rd, it being also possible for C to execute C.f;

f() instead of C.f;

s() in order to forward a message received in C.f.rd back to its sender or senders, possibly with some modifications, C.f;

f() not switching the read/write memories, cell C itself evaluating the protocol, C.f.protocol, associated with port C.f, in order to send off or forward the response message with no need for message scheduling or synchronization sessions, TICC™

-Ppde providing methods for executing all kinds of TIPs at functionPorts, as discussion in Sections 2 and 4 of Chapter 3;

methods(3.5), simple TIP execution at a generalPort;

Supposing C.p in (C.1) is a generalPort C.g of cell C, C being the unique parent cell of C.g, C being the only cell that may use C.g, generalPort C.g being used by cell C to send out service request messages and receive response messages, C executing C.p;

<

guard>

?()=C.p;

pR?() (‘

pR?()’

for ‘

pathway Ready?’

) in (C.1), C.p;

pR?() returning truth value true, cell C then executing C.p;

tip()=C.g;

tip()=C.g;

x().s() (‘

x()’

for ‘

construct’

), the pthread C.g;

x() being the abstraction whose refined form is executed by C in the executionMemory, C.g.ex, of C.g.vM, C.g;

x() being executed in order to compute, construct and write a service request message in C.g.wr, and immediately thereafter C itself executing C.g;

s() to invoke and execute eval(C.g.protocol), in order to send that service request message in C.g.wr to one or more ports, C′

.q, the read/write memories of C.g.vM being switched before message delivery so that each C′

.q receives the service request message in its readMemory C′

.q.rd, it being also possible for C to execute C.g;

f() instead of C.g;

s() in order to forward a message received in C.g.rd back to its sender or senders, possibly with some modifications, without switching the read/write memories, cell C itself evaluating the protocol, C.g.protocol, associated with port C.g, in order to send off or forward the message with no need for message scheduling or synchronization sessions, TICC™

-Ppde providing methods for executing all kinds of TIPs at generalPorts;

methods(3.6), for defining five kinds of synchronous TIPs;

the five kinds of TIPs being, (i) simple TIPs introduced in statements (C.1) and (C.2), (ii) spawning TIPs that spawn computations in other cells in A;

cells() in order to respond to a service request, spawning TIPs being introduced in Sections 4.1 and 4.2 of CHAPTER 3 in statements (4.1) through (4.3) and statements (4.11) through (4.13), (iii) TIPs servicing port-vectors, introduced in Section 4.2 of CHAPTER 3, in statements (4.8) through (4.13), (iv) TIPs with non-deterministic guards and existential guards, introduced in Section 4.4 of CHAPTER 3, in statements (4.14) and (4.16), (v) TIPs containing in its TIP-body other embedded TIPs, introduced in Section 4.5 CHAPTER 3, in statements (4.18) through (4.23), any embedded TIP being any one of these five kinds of TIPs, it thus being possible for all the above kinds of TIPs to appear in any combination in the TIP-body of a single TIP, these five kinds of synchronous TIPs and corresponding asynchronous TIPs being the only kinds of TIPs needed to design and build any TICC™

-Ppde software or hardware system, TICC™

-Ppde providing methods for defining all kinds of TIPs;

methods(3.7), for transaction completion;

ports C_i.p for 0≦

i<

n, in port-group pG synchronously delivering a joint service request message m to all ports D_j.q in port-group qG for j, 0≦

j<

m, by simultaneous coordinated parallel execution of eval(C_i.p.protocol), for 0≦

i<

n, this parallel evaluation of C_i.p.protocol by each C_i being automatically coordinated by agents in pG.pathway, each port C_i.p being immediately locked soon after C_i begins evaluation of C_i.p.protocol, each port D_j.q being immediately locked when the parent cell D_j of D_j.q senses the message m delivered to D_j.q, thus preventing a second service request message from being received at D_j.q, the port D_j.q receiving delivery of a second service request message only after the first service request message m has been processed and responded to by all parent cells D_j by sending a joint response message, m′

, via all ports in qG, the port C_i.p sending a second service request message only after all parent cells C_i have sensed the joint response message m′

sent by qG, each parent cell D_j asynchronously evaluating the protocol, D_j.q.protocol, in parallel with other parent cells of ports in port-group qG, in order to send the response message m′

over the same group-to-group pathway, qG.pathway≡

pG.pathway, this parallel execution of said protocols by parent cells D_j being again coordinated by agents in qG.pathway, said agents guaranteeing simultaneous delivery of joint response message m′

exactly once to every port C_i.p in pG, sensing of this response message m′

received at ports C_i.p by parent cells C_i constituting for each C_i completion of the transaction that started when C_i.p sent its service request message m to D_j.q, thus each port in A;

ports() sending successive service request messages only after successive transaction completions and similarly each port in A;

ports() receiving successive service request messages only after successive transaction completions, each port always sending back response message via the same pathway through which that port received its service request message, TICC™

-Ppde providing methods for guaranteed orderly completion of all parallel transactions without mutual interference;

methods(3.8), for defining correctness of transactions;

transaction between any two ports p and q in A;

ports() being written as [p(srm(t₁))q(rm(t₂))], p(srm(t₁)) being the service request message sent by port p at time t₁ and q(rm(t₂))) being the response message sent back by port q at time t₂, the said transaction being correct if only if for all messages p(srm(t₁)) and g(rm(t₂)) the relation R_(p,q)(srm(t₁) rm(t₂)) is true, R_(p,q) being the name of a relation that is specific to the port pair (p,q) and in addition the timing restriction t₂−

t₁≦

τ

_max(p,q)) is also true τ

_max(p,q) being an upper bound on the delay that may occur before the transaction between p and q is completed, ports p and q being well-matched if and only if every transaction between p and q is correct, this well-matched property of ports being dependent on the TIPs, p;

TIP() and q;

TIP() and also being an important property in TICC™

-Ppde, the property being referred to several times in these claims, the timings and bounds associated with transactions being estimated at the time of design and verified after implementation of pthreads and conditions in the TIPs, fully refined A;

implementation() being correct if and only if all pairs of ports connected by pathways in A;

TICC™

-network() are well-matched, TICC™

-Ppde providing methods for validating satisfaction of well-matched property of pairs of ports connected by pathways in A;

implementation();

methods(3.9), for defining abstractions called CIPs;

a computer program called C;

CIP() (Cell Interaction Protocol of C) being specified by implementers for each cell C in A;

cells(), C;

CIP() specifying an initialization routine C;

CIP-init(), for the cell C, initialization being done only once, at the time C is started, C;

CIP-body() specifying the order in which C may poll its ports C.p and execute C.p;

tip() when appropriate for each one of its ports, C;

CIP-body() polling ports C.p of cell C cyclically one after the other, this cyclic polling and TIP execution being called the polling cycle of cell C, C continuing its polling cycle until C terminates its operations or C suspends its operations as a result of receipt of an interrupt message from another cell in A;

cells() at one of the interruptPorts of C, C being suspended only between successive TIP executions in its polling cycles, it being impossible to suspend a TIP execution in the middle of its execution unless programmed suspension is built into a TIP-body as discussed in Section 8.2 of Chapter 3, suspended C resuming execution later at the time next message is delivered to any of the ports of C, execution of C.p;

TIP() for any port C.p being not synchronized with message deliveries to C.p, polling C.p by cell C succeeding only if C.p had been delivered a message before the time at which C.p was polled in a polling cycle, message at C.p missed in one polling cycle being caught in the next polling cycle, C;

CIP() for each cell C running in parallel with C′

;

CIP() of all other cells C′

in A;

cells(), each cell being run in its own unique and distinct designated CPU, polling cycles of distinct cells in A;

cells() being not necessarily synchronized with each other, TICC™

-Ppde providing ad hoc synchronization and coordination methods, as described in Section 6.6 of CHAPTER 3, to coordinate and synchronize polling cycles of distinct cells in A;

cells() at any point during the implementation of application A without having to change any of the refinements done up to that point, A;

CIPS() being the set of all computer programs C;

CIP() for every cell C in A;

cells(), it being the responsibility of implementers to define C;

CIP() for each cell C in A;

cells() in a manner that is consistent with CIP definition formats in TICC™

-Ppde and intended functionality of cell C in A;

implementation(), TICC™

-Ppde providing methods for defining CIPs;

methods(3.10), two possible execution modes in polling cycles of CIPs;

C.p returning truth value true when it was polled by cell C causing C to follow one of two possible courses actions, (i) executing the TIP-body C.p;

tip() immediately and responding to the received message, or (ii) inserting C.p into a sortedPortsList of cell C, sorting usually being done based on time stamps at ports indicating message delivery times in the local clock of the CPU that runs the cell, such time stamps being set at the time of message delivery to ports by protocols that deliver messages to ports, or sorting being done according to any sorting relation local to cell C, after completing polling and sorting all its ports, C executing C.p;

tip() for each C.p in the sortedPortsList in the order it appears in the list, C.p returning truth value false when it was polled by cell C also causing C to follow one of two possible courses actions (i) skipping port C.p and immediately proceeding to poll its next port if the guard at C.p is an asynchronous guard, or (ii) waiting at port C.p for a message to arrive, executing C.p;

tip() after the message arrives and then only proceeding to poll its next port if the guard at C.p is a synchronous guard, it being also possible for a CIP to execute TIP-bodies at some of its ports immediately after the guard of the TIP returns truth value true and sort other ports into the sortedPortsList for later execution, TICC™

-Ppde providing methods to specify sorted/unsorted and synchronous/asynchronous executions of TIPs by CIPs;

methods(3.11), for defining and using port-groups;

port-groups being collections of ports belonging to distinct cells in A;

cells(), no two port-groups having any port in common, no two ports attached to the same cell being ever in a port-group, port-group being defined by connecting a group of distinct ports attached to distinct cells to an agent in a pathway, agents in each group-to-group pathway dispatching messages written jointly by parent cells of ports in a message sending port-group after all the said parent cells have completed writing their respective contributions to the joint message, the dispatched message being delivered synchronously to all ports in the message receiving port-group, dispatch and delivery of messages between ports in port-groups thus being always synchronous, agents in the pathway connecting port-groups coordinating all message dispatches and deliveries in the said pathway, agents also coordinating installation of corresponding message dispatch and delivery events in SMS (Self Monitoring System) and enforcing data security during message deliveries by delivering messages to ports only if the (port, message) pair satisfies an a priori specified security condition, each parent cell of ports in the message receiving port-group sensing and responding to the received message at its own time, even though the said message was synchronously delivered to all ports in the message receiving port-group, port-groups thus providing mechanisms in TICC™

-Ppde to implement synchronous forks and joins of parallel processes in application A, TICC™

-Ppde providing mechanisms to define port-groups and install group-to-group pathways, and providing protocols for message exchanges over all group-to-group pathways likely to be used in parallel programming, TICC™

-Ppde providing methods also for defining and using port-groups;

methods(3.12), for defining and using port-vectors;

cells having one or more port-vectors defined for them, each port-vector consisting of two or more ports attached to the same cell, ports in a port-vector being all of the same kind, either all generalPorts or all functionPorts or all interruptPorts, the notation C.p being used to refer to a port-vector of cell C, C.p=[C.p₁, C.p₂, . . . , C.p_k], k≧

2, parent cell of C.p polling the ports in C.p in every one of its polling cycles, each C.p_i for 1≦

i≦

k being connected to a distinct pathway, C.p_i.pathway, each C.p_i for 1≦

i≦

k receiving messages independently of each other through C.p_i.pathway from distinct cells other than C, in each polling cycle the parent cell responding to messages received at ports C.p_i only after all ports in C.p have received messages, else the parent cell skipping all ports in the port-vector C.p in that polling cycle, the simplest TIP at port-vector C.p having the form

Asynchronous C.p;

TIP( ) = (C.p₁;

mR?( ) &

C.p₂;

mR?( ) &

... &

 

 

 

 

 

 

C.p_k;

mR?( )){ C;

r(p);

C.p₁;

s( );

...;

C.p_k;

s( );

} or (C.3) Synchronous C.p;

TIP( ) = (C.p₁;

mR?( ) &

C.p₂;

mR?( ) &

... &

 

 

 

 

 

 

 

 

C.p_k;

mR?( ))*{ C;

r(p);

C.p₁;

s( );

...;

C.p_k;

s( );

}, (C.4)

 

where C;

r(p) is a pthread defined and executed in the private memory of cell C, C;

r(p) using messages received at every port C.p_i for 1≦

i≦

k, the received message residing in distinct virtualMemories C.p_i.vM for 1≦

i≦

k, each C.p;

TIP() responding unconditionally to every port in C.p, it being possible for C.p;

TIP() to be any one of the five kinds of TIP, port-vectors being used in applications both to implement asynchronous forks and joins of parallel pthread computations and to implement ad hoc synchronization and coordination of computations performed by cells as described in Section 6.6 of CHAPTER 3, TICC™

-Ppde providing methods for defining and using port-vectors;

methods(3.13), for group-to-group transactions;

each pathway in A;

implementation() being connected to a group of one or more message sending ports in a port-group, pG, each port in pG belonging to a distinct parent-cell, all ports in pG being connected to the same agent, a0, in the group-to-group pathway, pG.pathway, pG.pathway connecting ports in pG to a group of one or more other ports in another port-group qG, all ports in qG being connected to another agent, a1, in qG.pathway≡

pG.pathway, in a manner shown in FIG. 19, it being also possible that pG≡

qG and a0≡

a1 as shown in FIG. 17, the said pathway always transmitting message only in one direction, from parent cells of message sending port-group pG or qG to parent cells of message receiving port-group qG or pG, respectively, ports in a message sending port-group pG always sending a joint service request message to ports in port-group qG, ports in qG always sending back to ports in pG a joint response message through the same qG.pathway, ports in ports-groups pG and qG thus always exchanging only joint-messages jointly written and jointly synchronously received by all parent cells of ports in port-groups pG or qG, agents in pG.pathway≡

qG.pathway automatically guaranteeing coordinated dispatch and synchronous deliveries of all such joint-messages over the said pathway, agents also automatically coordinating installations of corresponding message dispatch and delivery events in SMS (Self-Monitoring System) for every message sent or received by every port in port-groups pG or qG, parent cell of each port in qG sensing and responding to the service request message at its own time in one of its polling cycles, polling cycles of different cells not being necessarily synchronized to each other or synchronized to message delivery times, each port in qG responding back to ports in pG via the same qG.pathway≡

pG.pathway, all ports in pG and qG having the same virtualMemory associated with them, pG.vM≡

qG.vM, a message exchange transaction between ports in pG and ports in qG being completed only when all parent cells of ports in pG have received and sensed the joint response message sent by parent cells of ports in qG, pG being well-matched to qG iff every port in pG is well-matched to every port in qG, TICC™

-Ppde thus providing methods for defining and using well-matched group-to-group transactions;

methods(3.14), for guaranteed timely transaction completions with predictable timings;

TICC™

-Ppde enabling timely completion of every transaction in application A with in predictable time bounds by, (i) guaranteeing, no cell C ever misses sensing any service request message delivered to any of its ports, C.p, (ii) automatically activating the TIP-body of C.p;

tip() at every port C.p of cell C in A;

cells() after C senses receipt of a service request at a port C.p, (iii) making it impossible for any process or cell in A;

implementation() or outside A;

implementation() to interrupt execution of C.p;

tip() once it has been activated, (iv) guaranteeing completion of every transaction started by receipt of service request message at any port C.p, (v) guaranteeing predictable timely response to every received service request at every port C.p of every cell C in A;

cells() through elimination of instruction scheduling delays in CPUs that might be caused by use of speed-up techniques such as multiple instruction-stream executions, look-ahead scheduling, pipe-lined processing and cached executions, or any other kind of ornamentation of instruction scheduling in CPUs, these speed up techniques being not necessary in TICC™

-Ppde parallel programs to gain high throughputs, high throughputs being achieved in TICC™

-Ppde parallel programs through arbitrary scaling of small grain size parallel processes, execution of any C.p;

tip() taking no greater than 10 to 100 microseconds to complete, (vi) transaction completions being always caused only by TIP executions, (vii) transaction scheduling and coordination being always caused automatically by orderings of ports in polling cycles of cells in A;

cells() and orderings of TIP executions induced by orderings of message deliveries to ports in A;

ports(), (viii) transaction synchronization being always caused by automatic synchronization of message deliveries in group-to-group transactions and use of ad hoc synchronization techniques described in Section 6.6 of CHAPTER 3, (ix) all TIP executions in A;

implementation() being self-synchronizing and self-coordinating, (x) implementers being responsible only to define C.p;

TIP() for every port C.p in A;

ports() using TIP formats provided by TICC™

-Ppde for various kinds of TIPs making sure every pair of ports connected by a pathway is well-matched and define C;

CIP() for every cell C in A;

cells() consistent with CIP definition formats in TICC™

-Ppde and intended functionality of each C;

CIP(), (xi) all message exchanges in A;

TICC™

-network() being self-synchronizing and self-coordinating, (xii) all of these features together providing guaranteed timely transaction completions with predictable timings for all transactions in A;

implementation(), TICC™

-Ppde thus providing methods for guaranteed timely transaction completions;

methods(3.15), for tuning preservation;

guaranteed and timely transaction completions in turn maintaining and guaranteeing mutual tuning of components in each pathway in A;

pathways() that exchange signals with each other, state changes caused in the components of a pathway by signal exchanges during message transmission in one direction causing all components in the pathway to be ready for message transmission in the other direction, and message transmission in the other direction automatically resetting said states of all components in the pathway to their well tuned initial states, as described in Section 1.2 of CHAPTER 3, thereby always guaranteeing high-seed asynchronous communications in A;

implementation() with no need for synchronization sessions, TICC™

-Ppde thus providing methods for automatic tuning preservation;

methods(3.16), for coordinating joint processing of messages in virtualMemories by parent cells of ports in port-groups;

all ports C_i.p in a port-group pG for 0≦

i<

n, always having an identical message delivered to them synchronously and this message residing in the readMemory C_i.p.rd≡

pG.rd, both the message and the readMemory being common to all ports C_i.p in pG, the number of ports in pG usually being in the 1 to 16 range, parent-cells of ports in pG executing their respective C_i.p;

tip() in parallel in order to process and respond to the same message synchronously delivered to all of them, parent-cell of each C_i.p in pG responding to the received message in its own due course in one of its polling cycles, parent-cells C_i.p for 0≦

i<

n not necessarily responding to the received message synchronously, however, each parent-cell C_i executing C_i.p;

tip() in the same virtualMemory pG.vM≡

C_i.p.vM in parallel with parent-cells of all other ports in the port-group pG, virtualMemory pG.vM≡

C_i.p.vM providing a common scratchPad memory, pG.sp≡

C_i.p.sp, for all parent-cells C_i of ports C_i.p in order to exchange data with each other during such parallel C_i.p;

tip() executions, the parent-cells C_i achieving correct coordination by exchanging said data with each other through pG.sp during execution of C_i.p;

tip(), it being the responsibility of implementers to write computer programs for pthreads in C_i.p;

tip() for ports C_i.p in pG enabling such coordination using pG.sp and install where necessary pthread locks to enforce coordinated updates of commonly shared data, such pthreads executed in parallel by parent-cells of ports in a port-group being the only pthreads in A;

pthreads() that may be mutually dependent on each other, TICC™

-Ppde thus providing facilities for coordinated joint parallel processing by cells in cell-groups;

methods(3.17), for completing A;

implementation();

methods for completing A;

implementation() through successive refinements of abstract TIPs and CIPs in A;

DESIGN(), and abstract Msg-subclass in A;

messages(), decomposition of compound cells, C, into sub-networks of cells interconnected by pathways and encapsulation of sub-network inside the compound cells, refinements thus consisting of defining computer programs that implement the abstract pthreads, abstract conditions and abstract Msg-subclasses and decomposition and encapsulation of compound cells, all pthreads defined as per rules of TICC™

-Ppde, all Msg-subclasses being defined satisfying formats given in top level abstract Message class of TICC™

-Ppde, the set of all pthreads, conditions, Msg-subclasses and encapsulated cells defined in A;

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

pthreads(), A;

conditions(), A;

messages() and A;

cells(), at each stage of refinement A;

implementation() containing A;

TICC-Network(), A;

TIPS(), A;

CIPS(), A;

messages(), A;

pthreads(), A;

conditions(), A;

definitions(), A;

cells and A;

requirements() defined up to that stage of refinement, A;

definitions() consisting of logical characterizations of all pthreads, methods and conditions, TICC™

-Ppde providing methods for successively refining abstract specifications and completing A;

implementation();

methods(3.18), mutual independence of TIPs associated with distinct cells and mutual independence of pthreads &

conditions appearing in those TIPs;

each TIP-body C.p;

tip() at a port C.p of a cell C in A;

cells() or TIP-body of a port-vector, C.p;

tip() being executed only by parent-cell C, all ports appearing in C.p;

TIP() and C.p;

TIP() being attached to the same parent-cell C, the virtualMemory C.p.vM providing the execution environment for executing C.p;

tip(), the private memory of parent-cell C providing the execution environment for executing the port-vector TIP-body, C.p;

tip(), during execution of C.p;

tip() or C.p;

tip() the cell C using only data and other methods defined in cell C and ports appearing in C.p;

TIP() or C.p;

TIP() and methods defined in software components in pathways connected to ports appearing in C.p;

TIP() or C.p;

TIP() and tuned to or attached to each other, the executed pthreads changing only data associated with parent cell C and ports used in the execution and nothing else, thus all pthread and TIP executions by distinct cells being mutually independent, excepting those pthreads that share data through scratchpad memory to coordinate parallel executions by parent-cells of ports in a port-group, at any stage of refinement using logical input/output characterizations of pthreads, methods and conditions described in validating computer programs of said pthreads, methods and conditions and for jointly validating computer programs of pthreads and conditions that share data through scratchpad, TICC™

-Ppde providing methods that exploit mutual independence of TIPs and pthreads in order to validate computer programs defining TIPs and pthreads;

methods(3.19), predicates used to describe states of software components;

state of any software component, x, being defined by Boolean combinations of predicates having the form (x.attribute=data), (x.attribute₁<

y.attribute₂), (x.attribute₁<

y.attribute₂), (x.attribute₁ε

y.attribute₂) or (x.attribute₁ε

y.attribute₂), etc., x and y being cell C, or a port C.p of cell C, or any component of C.p.pathway or any data item in C.p.rd;

msg() or C.p.wr;

msg(), C.p.rd;

msg() being the message in C.p.rd and C.p.wr;

msg() being the message in C.p.wr, states being used to define input/output characterizations computer programs defining pthreads, states being used also to define conditions implemented by computer programs, TICC™

-Ppde providing methods to characterize states of software components in A;

implementation();

methods(3.20), logical input/output characterizations of pthreads, methods and conditions;

for any pthread or method P(), its characterization having the form,

{pre_P-C?()(t₁) &

m;

C?()(t₁)}[P()(t₁)(t₂)]

{post_P-C?()(t₂) &

m′

;

C?()(t₂) &

R_P(m,m′

)(t₂) &

((t₂)≦

(t₁+τ

_max(P))}, 

 

(C.5)

 

pre_P-C?() and post_P-C?() being pre-condition and post-condition associated with P(), these conditions specifying states of software components in which the pthread P() is being executed, m;

C?() being the condition that characterizes the state pf input message m processed by P(), m′

;

C?() being the condition that characterizes the state of output message m′

produced by P(), R_p(m,m′

) being the relation between m and m′

that should be satisfied every time P() is executed, ‘

→

’

being the symbol that denotes execution of P(), execution of P() beginning at the same time t₁ when pre_P-C?() and m;

C?() become true, execution of P() terminating at time P() when all of post_P-C?(), m′

;

C?(), R_p(m,m′

) and ((t₂)≦

(t₁+τ

_max(P)) become true, τ

_max(P) being the maximum time it may take to complete execution of P(), each condition in (C.5) being a Boolean combination of states of one or more software components in which the condition is evaluated, the software components being all either attached to each other or tuned to each other, the computer program for P() being correct if and only if the logical characterization of P() given in (C.5) holds true, every time P() is executed, the definition of the computer program for a condition being correct if and only if evaluation of that computer program returns true if and only if the Boolean combination of predicates defining the said condition is true, the set of logical characterizations of all pthreads, methods and conditions in A;

implementation() defined during refinements being called A;

definitions(), TICC™

-Ppde providing interactive tools to characterize all pthreads and methods used in an implementation;

methods(3.21), cell isolation and program mobility;

an important property of TIP being, formats of TIPs defined at ports are independent of the kinds of pathways connected to those ports, TIPs integrating communications with computations in the sense each cell by itself evaluates protocols associated will all of its ports, there being no difference between computations performed by a cell to process and build messages and computations performed by the same cell to transmit messages, message processing/building computations and protocol evaluations in a TIP-body never being interleaved with each other, protocol evaluations always occurring only after all computations to process and build messages have been completed in the TIP-body, TIPs thus isolating communications from computations performed by cells in each TIP-body, TIPs also isolating parallel computations performed by different cells in A;

cells(), the protocol at a port being always executed in the virtualMemory of that port, data defining state of cell C being held in the private memory of cell C, and data defining states of ports attached to cell C being held in the respective virtualMemories of those ports, the virtualMemories and private memories of cells C thus providing distinct execution environments for distinct cells, two distinct cells in A;

cells() that are not parent-cells of ports in a port-group being able to execute in parallel at the same time copies of the same pthread or protocol in distinct virtualMemories or distinct private memories of cells, parent-cells of ports in a port-group being able to execute in parallel at the same time the same pthread in the same virtualMemory commonly shared by all ports in the port-group, execution of pthreads and protocols always changing only the states of cells that perform those executions and states of pathways associated with protocols and nothing else, thereby isolating parallel computations performed by cells in A;

cells() from each other, cell isolation enabling program mobility in a parallel computing system between two ports C₁.p and C₂.p of distinct cells C₁ and C₂ with distinct virtualMemories C₁.p.vM and C₂.p.vM, program mobility being achieved by transporting entire contents of the virtualMemory C₁.p.vM, with the state of the parent cell C₁ copied into C₁.p.vM, to the virtualMemory C₂.p.vM, TICC™

-Ppde thus guaranteeing cell isolation and program mobility;

methods(3.22), dependent and independent ports of cells;

each cell C in A;

cells() having multiple generalPorts, functionPorts and interruptPorts, a port C.p or a port-vector C.p of cell C being independent only if computations performed during execution of C.p;

tip() or C;

tip(C.p) depend only on message(s) delivered to C.p or C.p and the state of C.p or C.p and nothing else, it being possible for cell C to have more than one such independent port or port-vector, in all other cases ports of C being dependent on each other, the simplest C.p;

tip() for port C.p dependent on port C.q having the form C.p;

mR?(){C.p;

r(C.q).s();

} with the pthread C.p;

r(C.q) being used for processing and responding to message received at port C.p, the pthread C.p;

r(C.q) having C.q as its argument, this argument enabling C.p;

r(C.q) to use the current state of C.q and messages in C.q.vM as well as state of C.p and messages in C.p.vM while responding to message received at C.p, it being possible for more than one port to appear in the argument of such a response method C.p;

r(C.q), execution of TIPs at dependent port being coordinated as described in Section 4.5 of CHAPTER 3, it being possible to move dependent and independent ports from one cell to another duplicate of that cell in certain cases, as described in the said Section 4.5, TICC™

-Ppde providing methods to define TIPs so that all port dependencies are properly taken care of;

methods(3.23) for interrupt handling;

no Operating System may ever interrupt computations being performed by any cell C in A;

cells(), cell C being interrupted only through receipt of interrupt messages at its interruptPorts, such interrupt messages being sent to cell C by other cells in A;

cells(), receipt of interrupt messages at interruptPorts of cell C being serviced by cell C only once in each polling cycle, or each interruptPort signaling the CPU that runs cell C using CCP (Causal Communication Primitive) at the time an interrupt message is delivered to it and the CPU responding to it only between successive TIP executions, low grain size TIP executions, made possible by low message exchange latencies in hundreds of nanosecond range, enabling interrupts to be responded to with no more than 10 to 100 microseconds delays even though interrupts are processed only between successive TIP executions, an interrupt message being received at an interruptPort of cell C causing cell C to perform any one of the following;

(i) suspending the operation of cell C at the end of its current TIP execution, the suspended operation being automatically resumed, at the next TIP to be processed, by receipt of next message at any port of the cell C, mechanisms for such suspension and resumption of computations in cells being automatically handled by cell C itself without need for Operating System intervention, (ii) dynamically changing the order of TIP executions in cell C, or (iii) terminating operation of cell C and releasing the CPU assigned to cell C, all of these happening only between successive TIP executions, it being the responsibility of implementers to ensure that cell C services all pending as yet unserviced service request messages received at its ports before termination, TICC™

-Ppde providing methods so that no TIP execution is ever interrupted while at the same time all interrupts are promptly attended to;

methods(3.24) for programmed suspensions;

a pthread in C.p;

tip() at a port C.p in cell C being programmed to suspend its execution in the middle of C.p;

tip() execution, cell C proceeding immediately to poll its next port after suspending its computations in C.p;

tip(), such programmed suspensions being caused because conditions in cell C necessary to make progress in C.p;

tip() execution not being satisfied at the time of suspension, suspended computations C.p;

tip() being resumed automatically in an ensuing polling cycle of cell C when the said necessary conditions become satisfied, TICC™

-Ppde providing tools for implementing such programmed suspensions, as discussed in Section 8.2 of Chapter 3;

methods(3.25) starting parallel computations in A;

implementation();

the environment cell, also called the configurator cell, used to set up A;

TICC™

-network() being used to start computations in application A, computations being started by a user clicking on the image of the environment cell displayed by TICC™

-GUI and selecting from a displayed menu the option to start computations, the environment cell responding to this selected option by sending predefined messages to designated ports of designated starting cells in A;

cells(), the protocols delivering the said messages to the said designated cells automatically activating said designated cells before message delivery, said designated cells running in CPUs assigned to them by TICC™

-Ppde, once activated said designated cells initializing themselves, if necessary, during such initializations installing the rest of A;

TICC™

-network() if necessary, thereafter each one of the said designated cells starting their, respective, polling cycles and during those polling cycles sensing the delivered messages, responding to them and causing computations to spawn over the rest of A;

TICC™

-network(), TICC™

-Ppde thus providing tools to start parallel computations;

methods(3.26) stopping parallel computations;

while cells in A;

cells() are running in their respective assigned CPUs certain designated cells in A;

cells(), responsible to terminate computations, send interrupt messages to the environment cell requesting the environment cell to terminate computations, these termination requests arriving at different interruptPorts of an interruptPort-vector of the environment cell, the interrupt messages arriving at the interruptPorts of the said port-vector at different times, the environment cell responding to the interrupt messages received at the said interruptPorts only after all the said interruptPorts have received interrupt messages, when all interruptPorts in the said vector have received interrupt messages the environment cell broadcasting a termination interrupt message to all cells in application A through one of its generalPorts, each cell in A;

cells() receiving the termination interrupt message terminating itself on sensing receipt of this termination interrupt message, each such cell terminating only after servicing all as yet unserviced pending messages at its ports and sending back before termination a response message to the environment cell acknowledging receipt of the termination interrupt message, agent on the pathway connecting cells in A;

cells() to the environment cell coordinating all such responses and forwarding to the environment cell an acknowledgement message only after all cells in A;

cells() that received the termination interrupt message have responded to that interrupt message, and on receipt of this acknowledgement from all other cells in A;

cells() the environment cell terminating itself, if necessary, TICC™

-Ppde thus providing tools to stop parallel computations;

methods(3.27), for defining privileges;

each cell C in A;

cells() having the ability to dynamically install new ports C.q on itself, install other cells C′

in A;

cells(), and install pathways between said port C.q and ports C′

.p of newly installed cell C′

, cells C sending requests to install such new cells and pathways to configurator cells in application A, it being possible for an application to have more than one configurator cell, the configurator receiving such requests checking first whether the cell or cells that requested such installations have the requisite privileges to have the installations performed, servicing the installation request only if requisite privileges are satisfied, and then responding to the requesting cells appropriate responses, if requisite privileges are not satisfied then informing the requesting cells about privilege violations, installation of a new cell or a new pathway taking about 250 microseconds to one millisecond in a 2 gigahertz CPU, depending upon the number of ports and cells in the installation, installation of a new port taking about 30 to 50 microseconds in a 2 gigahertz CPU, configurators issuing privilege violation reports when privileges are violated, implementers having the responsibility to define privileges for cells in A;

cells() associated with ports that connect the cells to configurators in application A in manners that satisfy privilege definition formats in TICC™

-Ppde, it being possible to preinstall spare cells, ports, agents, virtualMemories and pathways of various kinds and keep them in a reserve pool, to be used as needed by configurators in application A, thereby speeding up considerably dynamic installations of such components, TICC™

-Ppde providing tools for defining privileges associated with ports in A;

ports();

methods(3.28), for defining security functions;

as specified in Section 7 of CHAPTER 3, an agent in a pathway delivers message to a port only if the port satisfies an a priori specified security condition for that message, agent issuing a security violation report if specified security condition is violated at the port, all message exchange latencies including in them times needed for such security checks, implementers of application A having the responsibility to define needed security functions as per specifications in TICC™

-Ppde, TICC™

-Ppde providing tools to define security functions;

methods(3.29), accessing external data from secondary storage devices and Internet;

every application A having certain number of cells in A;

cells() dedicated to access data from secondary storage devices and/or Internet and distributing them to virtualMemories of ports requesting such data, cells either sending requests for such data to a configurator, which forwards the data request to a cell dedicated to obtaining such data after checking privileges of cells that requested such data, or cells already having requisite privileges installing dedicated new generalPorts on themselves, setting up pathways from those generalPorts to cells dedicated to obtaining such data, cells sending requests for data via the newly established pathways and getting the needed data in return, only if a priori specified security functions for that requested data are satisfied, TICC™

-Ppde thus providing tools to access external data;

methods(3.30), for dynamic monitoring of an application while it is running using break points;

while examining activities of SMS (Self-Monitoring System) using TICC™

-GUI in order to monitor a running application is certainly possible, such monitoring will not present users data associated with events registered by SMS, thus there is a need for users to insert break points into TIPs C.p;

tip() in order to examine data associated with events registered in the SMS, installation of break points being illustrated here for simple TIPs having the form, C.p;

TIP()=C.p;

guard?(){C.p;

r().s();

}, introduction of such break-points requiring appending to C.p;

tip() the phrase, C.g;

pR?(){C.g;

b().s();

} as in the modified C.p;

TIP() shown below,

C.p;

TIP()=C.p;

guard?(){C.p;

r().s();

C.g;

pR?(){C.g;

b(C, C.p).s();

}},

 

C.g being a free unused generalPort of cell C, a pathway, C.g.pathway being dynamically established between port C.g and a functionPort of a configurator, the pthread C.g;

b(C,C.p) being the break-point method, C.g;

b(C,C.p) reading and writing into the virtualMemory C.g.vM the states of cell C and port C.p and also writing into C.g.vM messages processed by or built by C.p;

tip() at the time C.g;

b(C, C.p) was executed, cell C sending off the message written into C.g.vM to the configurator, the configurator causing the received data to be displayed on a screen of TICC™

-GUI, it being possible to insert such break-points in to TIPs of all kinds, however, since using break-points in this manner always disrupting timings of events occurring in application A, such break-points being used only in a testing mode of application A, TICC™

-Ppde providing tools to define and install such break-points in TIPs;

methods(3.31), for encapsulating sub-networks of A;

TICC™

-network();

TICC™

-Ppde providing methods to encapsulate sub-networks of A;

TICC™

-network() associated with subsystems, B, of application A into compound-cells, the sub-network encapsulated in a compound-cell for a subsystem B of application A being called B;

TICC™

-network(), the compound cell encapsulating B;

TICC™

-network() being called the compound-cell B, B having two kinds of ports, internal-ports and external-ports, internal-points being the ports attached cells in B;

TICC™

-network() and external-ports being the ports attached to the compound-cell B, there being a subset of cells in B;

TICC™

-network() containing internal-ports that are connected to external-ports of B by branches, each internal-port being so connected exactly to one external-port of B, it being possible to connect internal ports in a port-group inside the compound cell B to an external port of B through an internal agent of the compound cell B, the external-ports transmitting immediately signals they receive to the internal-ports they are connected to, distinct parent-cells in B;

TICC™

-network() with ports connected to external-ports of B sensing and responding in parallel to signals they receive from the external-ports, all other internal-ports of B not so connected to external-ports of B being connected to each other by internal TICC™

-Ppde sm-pathways, compound cell B hiding all components of B;

TICC™

-network() excepting the internal-ports connected to external-ports of B, from other cells in A;

TICC™

-network(), the set of TIPs B.p;

TIP() at each external-port B.p of a compound cell, B, being identical to the set of TIPs C.p;

TIP() defined at the internal-ports connected to B.p, such encapsulated compound cells, B, each with its own built-in SMS (Self-Monitoring System), being used as a software component, which may be plugged into larger software systems, connecting each external-port B.p of compound-cell B by a pathway to a port D.q of a cell D in the larger software system external to B, making sure every pair of ports, (B.p, D.q) is well-matched, ability to thus plug-in encapsulated components into larger networks enabling reuse of software subsystems, examples of such compound cells being illustrated in Section 2.2 of CHAPTER 3, TICC™

-Ppde providing tools to encapsulate sub-networks of a TICC™

-network.

4. methods recited in claims 1, 2 or 3, further including following additional methods pertaining to design of CPUs in multi-core chips in order to efficiently run A:

implementation();

methods(4.1), for simplification of CPU designs and special CPU requirements;

TICC™

-Ppde simplifying designs of CPUs by eliminating the need to use speed up techniques such as cached executions, multiple instruction stream executions, look-ahead scheduling of instructions and pipe-lined processing, as explained in Section 4.6 of CHAPTER 3, but TICC™

-Ppde requiring a small number of special facilities in each CPU running cells in A;

cells(), the said special facilities being (i) a hardware clock in each CPU to enable time stamping of message deliveries to ports attached to a cell run by that CPU, time stamping being done at times when messages are delivered to said ports, messages being delivered in parallel to the ports of said cell, multiple simultaneous message deliveries to multiple ports of said cell being possible, such multiple simultaneous message deliveries to multiple ports requiring facilities for the hardware clock of a CPU to be interrogated simultaneously by said multiple ports of said cell in order to set time stamps at times of message deliveries (details in Section 8.1 of Chapter

     3), (ii) requiring each such CPU to implement CCP (Causal Communication Primitive) as a hardware instruction, (iii) requiring interrupt handling facilities so that each interruptPort may communicate directly using CCP (Causal Communication Primitive) with the CPU running the parent-cell of said interruptPort, the CPU responding to received interrupt signal only between successive TIP executions of the said cell, and (iv) requiring each SMP (Shared-Memory Multi-processor) multi-core chip with multiple SMPs of the order of 256 or more in a single chip to have the shared-memory organized with SMMs (Shared-Memory Modules) that exploit virtualMemory organization in TICC™

-Ppde software systems, these requirements not complicating CPU designs, but however, complicating chip designs, simplified CPU designs increasing achievable CPU densities in multi-core chips, tools provided by TICC™

-Ppde to organize and execute parallel computations thus simplifying CPU designs without compromising execution efficiencies;

methods(4.2), for exploiting virtualMemory organization;

designing each CPU in an SMP with only a small private memory of no more than 10 kilo-words to 1 mega-word, but implementing each CPU with a capability to dynamically connect to any one of a collection of independent hardware memory modules using programmable logic networks, these memory modules being called SMM (Shared-Memory Modules), SMMs being kept in a pool of such hardware devices, each SMM in the pool having memory capacities in the range of 10 kilo-words to 1 giga-word or more, each SMM in the pool allowing no more than about 16 CPUs to simultaneously access it, assignment of SMMs to virtualMemories being done at compile time or run time, each port C.p of each cell C in A;

cells() of an application A dynamically connecting the CPU, C.cpu, assigned to parent-cell C of C.p to the SMM assigned to the virtualMemory C.p.vM at compile time or CPU assignment time, granting access to data in C.p.vM to C.cpu only at times when the state of port C.p, C.p.state=S and only during execution of C.p;

tip(), terminating the access immediately after C.p;

tip() execution is completed (details in Section 8.2 of Chapter

     3), and possibly connecting the same CPU to another SMM associated with the next port of cell C, this scheme enabling high-speed shared-memory accesses with reduced memory interference, dramatically minimizing memory contention in parallel shared-memory software systems running in multi-core chips with large numbers of CPUs of the order of 256 or more, providing intrinsic data protection, data privacy and system security to any application A, this scheme, however, requiring a memory organization with multiple memory-buses, one for each SMM, each SMM being simultaneously addressable by independently running CPUs connected to them, and programmable logic networks for efficiently dynamically changing connections between CPUs and SMMs at run times, SMMs eliminating once and for all the damaging legacy of organizing CPUs in SMPs with huge shared main memories of tens or hundreds of giga-words sizes, simplifying CPU designs, but complicating chip-designs, while at the same time intrinsically contributing to greater efficiency, greater software security, greater privacy and greater protection, TICC™

-Ppde thus enabling arbitrarily scalable secure protected parallel computations;

methods(4.3), for asynchronous hardware subsystem encapsulation;

it being possible to use the same techniques of design, implementation through refinement, requirements specification, formal verification and self-monitoring to implement any asynchronous hardware system, it being possible to use TICC™

-Ppde encapsulation techniques to encapsulate hardware subsystems into compound-cells, each such compound-cell having its own SMS (Self-Monitoring System), hiding all encapsulated components from other components in a hardware system, each such compound-cell itself being used as a hardware system component, being plugged into larger hardware systems in contexts where all external-ports of the compound-cell are well-matched to ports of the larger system to which they are connected, thereby facilitating fabrication of multi-core chips, TICC™

-Ppde being thus used to design and implement asynchronous hardware systems as well;

5. Methods as recited in claims 1, 2, 3 or 4 further including following methods for formally validating A:

implementation();

methods(5.1), for deriving A;

ALLEOPS() from A;

implementation();

methods to automatically derive from A;

DESIGN() and A;

implementation(), at each stage of refinement of A;

implementation(), ALLEOPs (ALLowed Event Occurrence Patterns) models of computations specified in the design and implementation, these models making explicit all event classes implicit in A;

DESIGN() and A;

implementation(), exhibiting causal chains of said event classes, ALLEOPs models also exhibiting patterns of event classes that may occur in computations specified in the design and implementation, multiple event instances of each event class in ALLEOPs occurring in computations while A is being run, there being two kinds of event classes in ALLEOPs, one kind called action event classes of the form X, action event being evaluation of a statement in a programming language, or evaluation of a condition, or evaluation of a pthread, the other kind of event class being called communication event classes having the form C.p^S[T(C.p,#)] for port C.p sending a message or C.p^F[T(C.p, #)] for port C.p forwarding a message and C′

.q^D[T(C.p,#)] for C.p delivering message to another port C′

.q, the terms T(C.p,#) appearing in communication event classes being called time-maps, each T(C.p,#) referring to a sequence of time instances t₁<

t₂<

. . . <

t_n, n≧

0, at which instances of the said event classes C.p^S, or C.p^F or C′

.q^D occur in a run of A;

implementation(), the number sign, #, 0≦

#<

n≧

0, (n−

1) being the total number of times time-maps with port C.p occurs in a CIP (Cell Interaction Protocol), symbols X and Y being hereafter used to refer to any of the said event classes, often omitting the tip-maps when not needed, symbols X and Y or X(t) and Y(t) being used to refer to instances of event classes, t being the time at which the instances occur, pairs of action event or communication event classes X and Y in ALLEOPs being linked by weighted directed causal-links having the form, X^C(X,Y)→

Y, other pairs of event classes in ALLEOPs being linked by causal-links without weights as in X(t)→

Y(t), yet other pairs of event classes in ALLEOPs not being so linked by any causal-link, the causal-link with weight C(X,Y) being interpreted as described later below, multiple instances X(t) for t=t₁<

t₂<

. . . <

t_n, n≧

1, of each event class in ALLEOPs occurring while A is being run, TICC™

-Ppde providing methods for automatically deriving A;

ALLEOPS() from A;

implementation() as defined and illustrated in Section 2 of CHAPTER 3;

methods(5.2), for deriving port-ALLEOPs;

methods for automatically deriving port-ALLEOP, C.p;

port-ALLEOP() from C.p;

TIP(), port-ALLEOP being the ALLEOPs model for C.p;

TIP() in A;

TIPS(), C.p;

port-ALLEOP() having the form,

C.p;

port-ALLEOP()=C.p;

ALLEOP-guard?(){C.p;

ALLEOP-body()}, 

 

(C.6)

 

methods used for automatic derivation of C.p;

port-ALLEOP() from C.p;

TIP() being described in Section 2 of CHAPTER 3 and illustrated using a sample application called BILL-BEN application, C.p;

port-ALLEOP()s providing conveniently modularized descriptions of ALLEOPs of A;

implementation() ;

methods(5.3), for building ALLEOPs graphs;

the graph of all port-ALLEOPs C.p;

port-ALLEOP() in BILL-BEN;

ALLEOPS() being illustrated in FIG. 6A, the graph being obtained by linking port-ALLEOP pairs, C₁.p;

port-ALLEOP() and C₂.q;

port-ALLEOP() for ports C₁.p and C₂.q attached to distinct cells C₁ and C₂ in BILL-BEN;

cells(), with weighted directed causal-links ^C(X,Y)→

or directed causal-links →

without weights, in a manner that is consistent with pathway interconnections specified in BILL-BEN;

TICC™

-network() and TIPs in BILL-BEN;

TIPS(), causal-links representing an irreflexive, transitive and asymmetric causation relation, all event classes in port-ALLEOPs with causal-links interconnecting them and time-maps associated with communication event classes being derived automatically by TICC™

-Ppde from specifications in A;

implementation(), the graph in said FIG. 6A being a representation of BILL-BEN;

ALLEOPS(), TICC™

-Ppde providing methods to automatically derive A;

ALLEOPS() from A;

implementation() for any application A and construct for any application, A, the graphical representation of A;

ALLEOPS() like the one shown in said FIG. 6A;

methods(5.4), for interpretation of causal links in ALLEOPs graphs;

each weighted directed causal-link having the form X^C(X,Y)→

Y appearing in ALLEOPs graphs representing a conditional causal-link, each directed causal-link of the form X→

Y appearing in said ALLEOPs graphs representing an unconditional causal-link, these causal-links being interpreted as follows;

if occurrence of an event instance X(t₁) of event class X at time t₁ causes an event instance Y(t₂) of event class Y to occur later at time t₂ in a run of A;

implementation(), written as X(t₁)→

Y(t₂), then there should exist either a conditional-causal link X^C(X,Y)→

Y or an unconditional causal-link X→

Y in the graphical representation of A;

ALLEOPS() such that Y(t₂) is an instance of Y and condition C(X,Y) is true at time t₂ in the case of conditional causal-link or instance Y(t₂) of Y occurs unconditionally in the case of unconditional causal-link, and in all cases, t₂−

t₂≦

τ

(X,Y), the upper bound τ

(X,Y) being the maximum allowed delay between occurrences of the two events X(t₁) and Y(t₂) in X(t₁)→

Y(t₂), the execution characteristics of parallel programs in TICC™

-Ppde making it possible to predict event occurrences with in precisely defined time bounds, the upper bounds τ

(X,Y) being first estimated by implementers of A from intended or measured running times of pthread and protocol executions and later confirmed after experimentation with the completed A;

implementation(), TICC™

-Ppde providing tools to correctly interpret ALLEOP graphs;

methods(5.5), for building the causalnet;

the network of event instances of all and only the communication event classes in ALLEOPs, with causal-links among them, generated automatically by the SMS (Self-Monitoring System) of TICC™

-Ppde during a run of A;

implementation() being called the causalnet of A in that run, representation of the set of all possible causalnets that may occur in any run of application A being called A;

domain(), the causalnets for the BILL-BEN example being illustrated in FIGS. 6B and 6C being examples of causalnet in BILL-BEN;

domain(), different runs of A producing different causalnets because of different conditions becoming true in different runs, not all ALLEOP-nodes having instances occurring in the causalnet in any given run of A;

implementation(), (A;

CausalNet() satisfies A;

ALLEOPS()) being true if and only if the following logical condition holds true,

(A;

CausalNet( ) satisfies A;

ALLEOPS( ))  

[∵

(Communication-Event X[t(C.p, #)]) (X[t(C.p, #)]occurringIn  

A;

ALLEOPS( ))  

 

∴

(X,Y)∴

(TIME t₁,t₂)(X(t₁) instanceOf X) &

 

 

 

((X(t₁)→

Y(t₂)) occurring-in A;

CausalNet( ))]  

 

 

 

[∴

(Communication-Event Y[TC′

.q, #)]) ∴

(TIME-INTERVAL  

 

 

 

τ

(X,Y))  

 

((X[T(C.p, #)] →

...→

Y[T(C′

.q,#)]) occursIn A;

ALLEOPS( )) &

 

 

 

(Y(t₂) instanceOf Y[T(C′

.q,#)]) &

 

 

 

 

 

 

(t₂ ≦

t₁ + τ

(X[T(C.p,#)],Y[T(C′

.q,#)]))], (C.7)

 

statement (C.7) asserting, A;

CausalNet() for application A satisfies A;

ALLEOPS() if and only if for every communication event instance X(t₁) of communication event class X[T(C.p,#)] in A;

ALLEOPS() and every causal-link (X(t₁)→

Y(t₂)) occurring in A;

CausalNet(), there is a communication event class Y[T(C′

.q,#)] in the graph of A;

ALLEOPS() with causal chain, (X[T(C.p,#)]→

. . . →

Y[T(C′

.q,#)]) such that Y(t₂) is an instance of Y[T(C′

.q,#)] and t₂≦

t₁+τ

(X[T(C′

.q,#)],Y[T(C′

.q,#)]), the causal chain (X[T(C.p,#)]→

. . . →

Y[T(C′

.q,#)]) signifying that there is a sequence of one or more event classes linked by causal-links leading to event class Y[T(C′

.q,#)] from event class X[T(C.p,#)] in ALLEOPs, ability to predict event occurrences in causalnets with in precisely specified time bounds making it possible to use TICC™

-Ppde platform to design, develop, implement, validate and run with self-monitoring applications for real time Cyber Physical Parallel Software Systems, TICC™

-Ppde providing tools to build causalnets and verify that said causalnets satisfy ALLEOPs associated with them in the sense of (C.7);

methods(5.6), for deriving automatically A;

port-TRACE()s from A;

port-ALLEOP()s;

traces generally describing what happens when a program is run, different programming disciplines using different formats to describe traces, traces in TICC™

-Ppde describing not only what may happen when A;

implementation() is run, but also specifying the semantics of action events occurring in a run of application A, semantics being specified by conditions under which an alternate in a collection of alternate events may occur in any given run, and specifying for each action event logical pre-conditions in application A which should hold true for that action event to occur and logical post-conditions application A that should hold true after the action event has occurred, as described in statement (C.5) and in Section 2 and Section 5 of CHAPTER 3 and illustrated in definitions shown in Appendices I through III of CHAPTER 3, the trace for a port-ALLEOP C.p;

port-ALLEOP() being called C.p;

port-trace(t_P), t_P being the virtual-time at which events in C.p;

port-trace(t_P) may begin occurring in a run of A;

implementation(), TICC™

-Ppde providing methods to automatically derive A;

port-TRACE()s from A;

port-ALLEOP()s using specifications in A;

implementation() and specifications in A;

definitions() given A;

implementation(), TICC™

-Ppde providing tools to automatically derive A;

port-TRACE()s from A;

port-ALLEOP()s and construct A;

domain();

methods(5.7), for deriving Automatically A;

ECT-network() from A;

domain();

port-ECT (port Event Characterization Table), C.p;

port-ECT(t_P), for a port C.p in A;

ports() being derived automatically by TICC™

-Ppde from C.p;

port-trace(t_P), C.p;

port-ECT(t_P) representing events occurring in C.p;

port-trace(t_P) in a tabular form that is convenient for formally proving CTL-assertions (Causal Temporal Language-assertions) given by implementers of A;

implementation(), several examples of C.p;

port-ECT(t_P) being presented in Chapter 3, an ECT-network being a network of any collection of port-ECTs C.p;

port-ECT(t_P) with specified initial conditions, interconnected to each other as per polling orders defined in CIPs of A;

CIPS() and message exchanges defined in C.p;

port-ALLEOP() of A;

ALLEOPS(), as illustrated in Tables 5 through 9, A;

ECT-domain() being the combined network containing C.p;

port-ECT(t_P) for all ports C.p in A;

ports(), TICC™

-Ppde providing tools to automatically derive ECT-networks from traces;

methods(5.8), for design verification;

TICC™

-Ppde automatically deriving ALLEOP models of A;

DESIGN() called A;

designALLEOPS() using abstract definitions in A;

TICC™

-network(), A;

TIPS() and A;

CIPS(), A;

designALLEOPS() making explicit, synchronization and coordination of all action and communication event classes and causal chains of event classes that were implicit in A;

DESIGN(), methods for deriving A;

designALLEOPS() from A;

DESIGN() being defined and illustrated in Section 2 of CHAPTER 3, A;

designTRACES() being derived automatically from A;

designALLEOPS(), methods for automatically deriving A;

designTRACES() from A;

designALLEOPS() being also defined and illustrated in said Section 2, A;

designTRACES() allowing users to tentatively associate timings and timing bounds with all event classes and verify synchronization and coordination of event classes as well as causal chains of event classes in A;

designTRACES(), A;

designECT-domain() being automatically derived from A;

designTRACES(), A;

designECT-domain() being used to formally validate designs, validation criteria being provided by implementers as CTL-assertions in A;

requirements(), TICC™

-Ppde developing formal proofs for CTL-assertions in A;

requirements() using A;

designECT-domain() in order to validate A;

DESIGN(), TICC™

-Ppde interacting with users during development of formal proofs, users providing guidance for proof search where necessary by providing additional CTL-assertions, methods for doing these being illustrated in Section 6 of CHAPTER 3, the formal validation methods being used to interactively generate counter examples when a required CTL-assertions are found to be not valid in A;

DESIGN(), implementer revising designs as needed using the counter examples and revalidating the design, such validations being also used to guarantee that A;

DESIGN() is free of deadlocks and livelocks, and guarantee progress in A;

DESIGN(), deadlocks stopping all operations in application A if they occur, livelocks, if they occur, freezing up some subsystems of A preventing them from performing their assigned tasks, while other subsystems are proceeding normally to perform their tasks, progress guaranteeing that causal chains of event instances of event classes occurring while application A is being run always satisfying specifications in A;

designALLEOPS() as defined in (C.7), TICC™

-Ppde providing tools to interactively verify given designs by evaluating CTL-assertions over A;

designECT-domain();

methods(5.9), for verifying correctness of pthreads;

each collection of computer programs for pthreads that interact with each other through a common scratchpad being jointly formally verified as being correct, computer programs for all other pthreads being independently formally verified as being correct, each computer program implementing a pthread or condition being formally verified to assure that the computer program satisfies the logical input/output characterization given in statement (C.5), this being possible because each pthread is a short computer program running only for about 10 to 100 microseconds, proving correctness of A;

implementation() requiring correctness of all pthreads in A;

implementation(), TICC™

-Ppde providing tools to interactively verify pthreads;

methods(5.10), for proving CTL-assertions given by implementers;

TICC™

-Ppde providing methods to develop interactive proofs of CTL-assertions (Causal Temporal Logic assertions), structure of CTL-assertions being informally defined in the last paragraph of Section 5.2 in CHAPTER 3 and examples of CTL-assertions appearing in Section 6 of CHAPTER 3, specific syntax of CTL-assertions being not as important as there being an unambiguous interpretation for any CTL-assertion, CTL-assertions given by implementers being validated by evaluating them over ECT-networks, evaluation of CTL-assertions over ECT-networks producing causal chains of events in the ECT-network that match with given CTL-assertions as per matching criteria defined and illustrated in Section 6 of CHAPTER 3, the process of generating causal chains of event instances in ECT-network that match with given CTL-assertions being called the proof checking process, guidance for proof checking being provided by users, methods for such interactive proof checking being illustrated in Section 6 of CHAPTER 3, CTL-assertions validated using ECT-networks being valid properties of A;

implementation() since the ECT-networks used in proof checking are all automatically derived from A;

implementation(), the valid CTL-assertions ultimately verifying the well-matched property of every pair of ports connected by a pathway in A;

implementation(), the well-matched property of pairs of ports connected by pathways in A;

implementation() following from proofs of the following;

(i) formal proofs of correctness of pthreads, (ii) formal proofs of progress in A;

implementation() indicating every causalnet in A;

domain() always satisfies A;

ALLEOPS() as defined in statement (C.7), (iii) formal proofs of all CTL-assertions in A;

requirements() for A;

DESIGN(), (iv) formal proofs that A;

implementation() is free of deadlocks, (v) formal proofs that A;

implementation() is free of livelocks, examples of such proofs being shown in Section 6 of CHAPTER 3, validation of A;

implementation() ultimately being dependent on the set of all validated CTL-assertions, TICC™

-Ppde providing tools to interactively verify CTL-assertions using ECT-networks;

methods(5.11), for providing guidance to implementers to identify CTL-assertions that validate A;

implementation();

guidance to implementers to define CTL-assertions needed to validate A;

implementation() being provided by A;

requirements() and the requirement specified in statement (C.8) below, A;

requirements() being logical specifications of requirements for application A specified in CTL-language by implementers before designing and implementing application A and updated during design and refinement, statement (C.8) providing guidance to specify CTL-assertions needed to verify correctness of A;

implementation();

[(A;

domain( ) satisfies A;

ALLEOPS( )) &

 

(A;

ALLEOPS( ) satisfies A;

requirements( ))] A;

implementation( ) is correct), (C.8)

 

implementers using criterion (C.8) and the requirement that all pairs of ports interconnected by a pathways should be well-matched, in order to ascertain they have not missed validating any needed CTL-assertions, TICC™

-Ppde providing methods to assist users by identifying ports connected by pathways that have not been validated as being well-matched, TICC™

-Ppde also assisting implementers to interactively identify counter examples that explain why given CTL-assertions are not valid in A;

implementation(), implementers using the counter examples to revise A;

implementation() as needed and revalidate the revised implementation;

methods(5.12), for ad hoc synchronization and coordination;

two events X(t₁) and Y(t₂) associated with two distinct cells in A;

cells() and occurring in the causalnet of A;

implementation() are incomparable in the sense (t₁≦

t₂) may be true in certain runs of A;

implementation() and (t₁>

t₂) may be true in certain other runs, it being possible, correct operation of A;

implementation() requires two such incomparable events X(t₁) and Y(t₂) to be either coordinated or synchronized, coordination of events X(t₁) and Y(t₂) meaning, one of them should always occur only after the other one has occurred, for example it may be required (t₁≦

t₂) should hold true in all runs of A;

implementation(), synchronization of events X(t₁) and Y(t₂) meaning (t₁=t₂) should hold true in all runs of A;

implementation(), TICC™

-Ppde providing ad hoc methods to coordinate and synchronize such incomparable events without having to change any of the refinements in A;

implementation(), such ad hoc synchronization and coordination methods requiring only that certain new pathways be established between certain newly installed ports of cells in which the incomparable events occur and defining or re-defining TIPs at ports associated with said cells in manners described in Section 6.6 of CHAPTER 3, it being possible to do such ad hoc coordination and synchronization also between any two groups of non-intersecting incomparable events in A;

implementation(), these ad hoc synchronization and coordination methods being unique to TICC™

-Ppde, not possible to implement in any other parallel programming paradigm without extensive revision of refinements, TICC™

-Ppde providing methods for such ad hoc synchronization and coordination.

6. Methods as recited in claims 1, 2, 3, 4 or 5 further including following SMS methods to dynamically build and analyze the causalnet while application is running, in parallel with the application:

methods(6.1), for driving the SMS (Self-Monitoring System);

statement (C.8) above providing the basis for operation of SMS in TICC™

-Ppde, agents embedded in pathways sending signals using CCPs (Causal Communication Primitives) to ports attached to EventBuilder cells (eb cells) of SMS to automatically install message dispatch and message delivery events in the growing causalnet of A;

implementation() while A;

implementation() is running, as described in Section 7 of CHAPTER 3, each eb cell being connected to a pathway through a distinct pair of ports in a port-vector attached to that eb cell, one port in the port-vector receiving signal from an agent in the pathway indicating message dispatch event occurring in the pathway, and the other port in the port-vector receiving signal from another agent in the pathway indicating the corresponding message delivery event in the same pathway, as indicated in FIG. 19, on sensing signals delivered to both ports in the said port-vector, the parent eb cell of the port-vector installing corresponding pairs of message dispatch and delivery event instances in the growing causalnet, such updating of the causalnet occurring while parent-cells C of ports C.p that received the delivered message are executing C.p;

tip(), time taken for installing the said event instances in the growing causalnet being one fiftieth to one hundredth the amount of time needed to execute C.p;

tip(), each eb cell being capable of servicing about ten to fifteen pathways, allowing for delays due to asynchronous executions in polling cycles of all cells, parallel updating of the growing causalnet by multiple eb cells being possible because each eb cell will be installing new communication events only in distinct non-intersecting branches of the causalnet, TICC™

-Ppde providing tools to automatically coordinate parallel computations performed by eb cells and ea cells, eb-cells communicating with ea-cells by exchanging signals using CCPs;

methods(6.2), for analyzing events in a growing causalnet;

EventAnalyzer cells (ea cells) in A;

cells() automatically checking whether the growing causalnet satisfies A;

ALLEOPS(), eb cells signaling ea cells every time they install new communication events in the causalnet, ea cells reporting an error every time the structure in the growing causalnet of A;

implementation() violates the structure of A;

ALLEOPS() by not satisfying statement (C.7), reporting an impending error when specified upper bounds on timings of event occurrences are violated for some events in the growing causalnet, or issuing alerts on identifying occurrences of a priori defined ALLEOPs event patterns in the growing causalnet, one or more ea cells being dedicated to monitor the growing causalnet for occurrences of a priori defined alert patterns, there being at least one ea cell for each eb cell in A;

implementation(), A;

cells() containing as many eb cells and ea cells as needed to guarantee operations in A;

implementation() with no interference with timings of events in A;

implementation(), all eb cells and ea cells operating in parallel and in parallel with all other cells in A;

cells(), with little or no interference with the operation of any cell in A;

cells(), TICC™

-Ppde providing tools to coordinate parallel computations performed by ea cells and eb cells by enabling eb cells and ea cells to communicate with each other by exchanging signals using CCPs;

methods(6.3), for self-diagnosis and self-repair;

SMS providing the basis for eventually building self-diagnosis and self-repair facilities in A;

implementation(), ea cells identifying errors or impending errors directly communicating with errant cells and using validated CTL-assertions containing events associated with the errant cells to diagnose and repair the errant cells or dynamically replacing them with new cells without interfering with normal operations in the rest of A;

TICC™

-network(), ea cells identifying a priori defined alert patterns responding to the identified alert patterns by dynamically changing parallel computations in a predetermined manner where necessary.

7. Methods as recited in claims 1, 2, 3, 4, 5 or 6 further including the following twelve programming abstractions introduced by TICC-Ppde, enabling abstract design, implementation of the design through successive refinements, the programming abstractions enabling efficient running of arbitrarily scalable massively parallel computing systems with automatic self-monitoring, the twelve abstractions being,

Abstraction(7.1), Cells:

cells being software abstractions of computing units of parallel programming software systems, cells enabling abstract specifications of parallel software system design, implementation through successive refinements, each cell running in a dedicated CPU (hardware ComPuting Unit), cells performing parallel computations by exchanging messages with each other, using their ports to send and receive messages via communication pathways interconnecting ports of cells, the graph of cells interconnected by pathways in application A being called A;

TICC™

-network(), cells being totally self-contained, not using an Operating System to assist their operations, TIC™

-Ppde providing tools enabling cells to perform all computations needed to build A;

TICC™

-network(), invoke and execute pthreads to process/construct messages they exchange with each other, invoke and execute protocols to send/deliver messages, and suspend/resume their operations on receipt of interrupt messages, with no assistance from any software not defined in the cell itself or software components attached to or tuned to the cell;

Abstraction(7.2), Pathways;

pathways being abstractions of communication channels, there being two kinds of pathways, sm-pathways and dm-pathways, sm-pathways interconnecting ports of cells running in an SMP (Shared-Memory multiprocessor), dm-pathways interconnecting ports of cells running in a DMP (Distributed-Memory multiprocessor), the computing nodes of the DMP being SMPs, each port in SMP, called the parent-cell of the port, each cell having multiple ports attached to it, each port of a cell being connected to only one unique pathway, multiple ports attached to distinct cells being connected to the same pathway, thereby enabling group-to-group communications, pathways containing agents and virtualMemories embedded in them, the same agent or virtualMemory never being embedded in more than one pathway, agents performing routing, synchronization and coordination of message traffic over the pathway in which they are embedded, agents also sending signals to SMS (Self-Monitoring System) to install message dispatch and message delivery events that occur in pathways they are embedded in, for any pathway, P, P;

ports() being the set of ports connected to P, P;

agents() and P;

virtualMemories() being the sets of agents and virtualMemories embedded in P, the union of the three sets P;

ports(), P;

agents() and P;

virtualMemories() being the pathway components of pathway P, no two distinct pathways ever having any pathway component in common, thereby pathways enabling simultaneous parallel message exchanges in A;

TICC™

-network() without message interference, TICC™

-Ppde providing tools to dynamically install cells and pathways in A;

TICC™

-network() while application A is running;

Abstraction(7.3), VirtualMemories;

software abstractions called virtualMemories being declared when pathways are installed, real hardware memory areas, or memory modules, being assigned to virtualMemories at compile time or run time of an application, each sm-pathway, S, having only one unique virtualMemory, S.vM, embedded in it, all ports p_i connected to any sm-pathway residing in the same SMP (Shared-memory Multi-Processor), all ports p_i connected to any sm-pathway S having the same virtualMemory, p_i.vM=S.vM associated with them, each dm-pathway, D, interconnecting port-groups, pG[j], residing in different and distinct SMPs, SMP[j], (Shared-Memory multi-Processor j) in a DMP (Distributed-Memory multi-Processor), each dm-pathway D having more than one virtualMemory embedded in it, one virtualMemory, pG[j].vM being tuned to port-group pG[j] in each SMP[j], pG[j].vM being identical to q_j.vM for all q_j in pG[j], virtualMemories p_i.vM and q_j.vM, holding messages transported via said pathways, said virtualMemories also holding pthreads and methods used by parent-cells of ports p_i and q_j, respectively, to process and create messages, in addition the said virtualMemories holding protocols, p_i.protocol and q_j.protocol, to transport messages over the pathways S and D, respectively, virtualMemories and pathways providing execution environments for all pthreads, methods and protocols they hold, virtualMemory organization contributing to data security privacy and integrity isolation of parallel computations performed by cells, efficient execution of parallel programs and simplification of shared-memory multi-processor designs for multi-core chips;

Abstraction(7.4), Protocols;

each port p connected to each pathway having a protocol, p.protocol, defined for it, only the parent-cell of p being allowed to execute p.protocol, execution of p.protocol by parent-cell of port p causing signals to be exchanged by pathway components, the signals exchanged by pathway components traveling over the pathway ultimately establishing a context in which message in p.vM is delivered to its intended recipients in sm-pathways or transported to its intended recipients via hardware signal transmission lines in dm-pathways, hardware agents embedded in dm-pathways also participating in protocol executions to transmit, coordinate, synchronize and route messages over dm-pathways said agents being embedded in, protocols enabling multiple simultaneous parallel message exchanges in an application limited only by the number of pathways in the application;

Abstraction(7.5), CCPs (Causal Communication Primitives);

CCPs being used to programmatically exchange signals between components in a pathway, each CCP being a statement in TICC™

-Ppde programming language having the form X;

x→

Y, X,Y being components embedded in a pathway, x being a signal transmitted by the CCP from X to Y, signals sent/received by components X,Y controlling the states of ndFSMs (non-deterministic Finite State Machines) embedded in X,Y, CCP being implemented either in software or in hardware, hardware CCP being implemented as a machine instruction in a CPU, each protocol being defined by concatenations of CCPs, such concatenations having the form X;

x₁→

Y;

x₂→

Z, X,Y,Z being all components in the same pathway, CCPs appearing in protocols being at times embedded in other programming statements of TICC™

-Ppde, software CCP taking only about 25 to 50 nanoseconds to execute in a 2-gigahertz CPU, hardware CCP taking only about 5 nanoseconds to execute in a 2-gigahertz CPU, CCPs being the central and most important abstraction introduced by TICC™

-Ppde, CCPs being solely responsible for making possible the parallel program organization in TICC™

-Ppde;

Abstraction(7.6), Tuning and Attachments;

all components of any pathway P exchanging signals, being always tuned to each other, tuning enabling each such component to be always ready to receive and respond immediately to signals they receive from other components of the pathway, thereby enabling guaranteed high-speed message exchanges via pathway P with latencies in the range of at most a few hundred nanoseconds with 2-gigahertz CPUs, tuning being a reflexive symmetric relation, any cell, C, being able to execute only methods or pthreads defined in C, or components embedded in any pathway connected to any port attached to C, C using only data defined in components attached C or data defined in components of said pathways, attachment being a reflexive, symmetric, transitive relation, tuning and attachment contributing to the modular object oriented organization of parallel software systems in TICC™

-Ppde;

Abstraction(7.7), Ports;

port is a software abstraction, each port p being attached to its unique parent-cell, port p having a unique virtualMemory, p.vM, associated with it, parent-cell of port p using p to send messages in p.vM to other cells via p.pathway connected to p and receive messages from other cells via the same p.pathway, each port p protecting data and methods in p.vM, by giving access to said data and methods only to its parent-cell and only when the parent-cell is ready to use those data and methods, terminating access after such use is completed, each port p having embedded in it a non-deterministic Finite state machine p.ndFsm with 2 states S (send) and R (receive), the states being used to coordinate message sending/receiving operations performed by the parent-cell of p, the states also being used to control access to virtualMemory p.vM by parent-cell of p, p.state=p.ndFsm.state, coordination and access control methods being described in FIGS. 1 through 4 of Section 1 of CHAPTER 3, parent-cell of p having access the virtualMemory p.vM to send message out via port p only when the state of p.state=S, port p receiving messages only when the state of p.state=R, ports in dm-pathways containing ndFsms having 4 states, S, S′

, R, R′

, two message sending state S and S′

, and two message receiving states R and R′

, ports not only sending and receiving messages but also controlling access to virtualMemories and thus protecting data and methods in virtualMemories, in addition making possible distributed organization of hardware Shared-Memory Modules, SMMs, which are dynamically assigned to virtualMemories and are used by CPUs as and when needed;

Abstraction(7.8), Agents;

agents in sm-pathways being software abstractions, agents being embedded in pathways, each agent, a, containing a 2-state ndFsm, a.ndFsm, embedded in it with states S (send) and R (receive), a.state=a.ndFsm.state, agents using their states to route, synchronize and coordinate message transmissions over pathways they are embedded in, as described in Section 1 of CHAPTER 3, FIGS. 2 through 4 and Section 7 of Chapter 3, agents also signaling components of SMS to dynamically install in the causalnet of a running application, message dispatch and message delivery events that occur in the pathways said agents are embedded in, as described in Section 7 of CHAPTER 3, dm-pathways containing hardware agents with 4 states, S, S′

, R, R′

, agents automatically synchronizing and coordinating all communications enforcing security and driving the self-monitoring system and thus slaving a unique and central role in TICC™

-Ppde;

Abstraction(7.9), TIPs (Thread Interaction Primitives);

TIPs being software abstractions that specify how the parent-cell of a port p in application A receives and responds to a message delivered to p, or how parent-cell checks readiness of a port p to send out a message, constructs message and sends it out via the port, every port attached to every cell in application A having a TIP defined for it, some TIPs being embedded in other TIPs, the set of all TIPs defined at the ports of a cell being used by that cell to perform parallel computations in application A, there being ten kinds of TIPs needed to specify all of parallel computations, 5 synchronous and 5 asynchronous, TIPs providing a compact modular specifications of interactions among cells, that can get as complicated as any computation can get the modular characterization of interactions provided by TIPs facilitating formal verification and validation of implementations of applications and cell isolation;

Abstraction(7.10), CIPs (Cell Interaction Protocols);

CIPs being software abstractions that specify how a cell initializes itself, polls its ports, processes messages delivered to its ports and responds to them, or creates new messages and sends them out via one or more of its ports, CIPs providing the basic processes that makes all parallel computations in TICC™

-Ppde possible;

Abstraction(7.11), A;

TICC™

-network();

A;

TICC™

-network() being a software abstraction of the control structure of the parallel computations in application A, A;

TICC™

-network() implicitly specifying synchronization and coordination of all computational and communication activities that occur during the parallel computations, just as the same sequential program may be run in different data structure definitions if the sequential program and data structure definitions are properly defined the same set of pthreads, A;

pthreads() of an application A may be run in different A;

TICC™

-network()s, if initialization routines in CIPs (Cell Interaction Protocols) are properly defined thereby enabling program optimization through chances in execution control structure;

Abstraction(7.12), The Self Monitoring System, SMS;

SMS being an abstraction that is unique to TICC™

-Ppde, SMS being a software abstraction of mechanisms used in TICC™

-Ppde to monitor the performance of a running application A, while it is running, in parallel with the application with no interference with timings of events occurring in the application, in order to detect and report errors in performance, pending errors and occurrences of a priori defined patterns of events while the application A is running, SMS using cell abstractions called eb cells (event builder cells) and ea cells (event analyzer cells) to build and constantly monitor the growing causalnet of a running application, SMS being a feature that is unique to TICC™

-Ppde.

8. Methods and abstractions as recited in claims 1, 2, 3, 4, 5, 6 or 7 further including five verification-abstractions introduced in TICC-Ppde, the verification-abstractions enabling TICC™

-Ppde to formally validate parallel programs and run them with automatic self-monitoring, the five verification methods and abstractions being,

Abstraction(8.1), Event Classes;

event classes being abstractions of computational and communication events occurring while an application A is running, each event class being a pair (name, t), there being two kinds of event classes, action event classes and communication event classes, name in an action event class denoting a statement in TICC™

-Programming language, or denoting a pthread, or denoting a condition in the parallel programs implementing application A, name in communication event classes having one of the forms, p^S, p^F, or p^D where p is the name of a port in application A, the superscript S signifying, the port p is sending out a message, superscript F signifying, port p is forwarding a message, and superscript D signifying, a message is being delivered to port p, t representing a sequence of time points at which event instances of the event class may occur in a run of application A, t being called the time-map of the named event class;

Abstraction(8.2), ALLowed Event Occurrence Patterns, ALLEOPs;

ALLEOPs representing abstractions of computational dependencies, said dependencies being expressed through a binary, irreflexive, asymmetric and transitive causal relation between event classes, ALLEOPs being the network of event classes connected to each other by conditional or unconditional directed arrows representing causal relations between pairs of event classes, a causal chain being a sequence of events connected by directed arrows (causal relations), the network of causal chains of event classes capturing patterns of computational event instances occurring in parallel programs for application A while application A is running, p;

port-ALLEOP() being the set of all causal chains of event classes occurring in p;

TIP(), C;

cell-ALLEOP() being the set of all causal chains of event classes occurring in C;

CIP(), A;

ALLEOPS() being the set of all causal chains of event classes occurring in application A;

Abstraction(8.3), Event Instances and Traces;

events, (name, t_i) for i=1, 2 . . . , n . . . being instances of the event class, (name, t), occurring at time instances t=[t₁, t₂, . . . , t_n, . . . ], n≧

0, while an application is running, there being no instance of event class (name, t) when n=0, pairs of event instances X(t_i) and Y(t_j) of respective event classes (X, t_x) and (Y, t_y) being connected to each other by a conditional or unconditional directed arrow representing causal relation only if its corresponding event classes are connected by such an arrow in ALLEOPs, the set of all possible causal chains of event instances occurring in any run of application A being called A;

TRACES(), A;

TRACES() being derived automatically from A;

ALLEOPS(), a representation of the set of all possible A;

TRACES() in application A being called A;

domain(), p;

port-trace(t_P) being the trace automatically derived from p;

port-ALLEOP(), C;

cell-trace(t_C) being the trace automatically derived from C;

cell-ALLEOP();

Abstraction(8.4), ECT-networks;

p;

port-ECT(t_P) being the Event Characterization Network consisting of ECT-blocks, representing causal chains of all event instances occurring in p;

port-trace(t_P) organized in a tabular form, port-ECTs being interconnected in a manner consistent with A;

TICC™

-network() and A;

ALLEOPS(), such ECT-networks facilitating formal interactive proof generation by TICC™

-Ppde, C;

cell-ECT(t_C) being the ECT-network corresponding to C;

cell-trace(t_C), A;

ECT-network() being the ECT-network corresponding to A;

TRACES();

Abstraction(8.5), Causalnets;

p;

port-causalnet(t_P) being an abstraction of p;

port-trace(t_P) containing only causal chains of communication event instances occurring in p;

port-trace(t_P), C;

cell-causalnet(t_C) being an abstraction of C;

cell-trace(t_C) containing only causal chains of communication event instances in C;

cell-trace(t_C), A;

causalnet() being an abstraction of A;

TRACES() containing only causal chains of communication event instances in A;

TRACES(), the SMS (Self-Monitoring System) generating automatically the causalnet of application A while it is running, in parallel with the run, automatically monitoring the dynamically growing causalnet to identify and report errors, pending errors and occurrences of a priori defined patterns of event instances.

9. Methods and abstractions as recited in claims 1, 2, 3, 4, 5, 6, 7, or further including following method to provide an integrated environment for design, development, verification and running with self-monitoring of applications, A:

TICC™

-Ppde itself performing CPU assignments to cells, cell activations in CPUs assigned to them, parallel process management, pthread management, communications, interrupt management, security enforcement, synchronization and coordination, without having to invoke an operating system or any other external software to perform any part of these service, TICC™

-Ppde using operating system in the current prototype implementations only for memory management, cache management and access to secondary storage devices and internet, it being possible to implement all of these services in TICC™

-Ppde itself with all needed operating system services being provided in parallel, thereby providing an environment for integrated design, development, verification and running of parallel software systems with self-monitoring.

10. Methods and abstractions as recited in claims 1, 2, 3, 4, 5, 6, 7, 8 or 9 further including following method to design, implement and run parallel programming applications, A:

any parallel computer program for any application A using any or all of the methods and abstractions recited in claim 1 through claim 9, using programmatic signal exchanges to organize and control parallel software systems, implemented in hardware or software, with or without formal validation and self-monitoring, or with only partial formal validation and partial self-monitoring.