Synthesis of large dynamic concurrent programs from dynamic specifications

Abstract

We present two methods for synthesizing large concurrent programs from temporal logic specifications. The first method deals with finite-state concurrent programs that are static, i.e., the set of processes is fixed. It produces an infinite family of static finite-state concurrent programs. The second method deals with dynamic concurrent programs, i.e., new processes can be created and added at run-time. It produces a single dynamic concurrent program. A dynamic concurrent program may be viewed as a limiting case of an infinite family of static programs, and so the second method may be viewed as generalizing the first. Our methods are algorithmically efficient, with complexity polynomial in the number of component processes (of the program) that are “alive” at any time. We do not explicitly construct the automata-theoretic product of all processes that are alive, thereby avoiding state explosion. Instead, for each interacting pair of processes, we construct (from a pair-specification) a pair-structure which embodies the interaction of the two processes. From each pair-structure, we synthesize a pair-program to coordinate the two processes. Our second method allows pair-programs to be added dynamically at run-time. They are then “composed conjunctively” with the currently alive pair-programs to “re-synthesize” the program. We can thus add new behaviors, which result in new properties being satisfied, at run-time. This “incremental composition” step has complexity independent of the total number of processes; it only requires the mechanical analysis of the two processes in the pair-program, and their immediate neighbors, i.e., the other processes which they interact directly with. Thus, any state-explosion incurred is explosion in the product of only two processes. We establish “large model” theorems which show that the synthesized global program inherits correctness properties from the pair-programs.

Appendix: Glossary of major symbols

$\models$ :

Satisfies relation of $\mathrm {CTL}^*$, Sect. 2.2

$\models _{\Phi }$ :

Satisfies relation of $\mathrm {CTL}^*$ relativized to fairness notion $\Phi$, Sect. 2.3

$\Phi$ :

$\mathrm {CTL}^*$ path formula that specifies fairness, Sect. 2.3

$\otimes , \bigotimes _{j \in I(i)}$ :

“Conjunctive” guarded-command composition operator, Definition 14

$\oplus , \bigoplus _{\ell \in [1:n]}$ :

“Disjunctive” guarded-command composition operator, Definition 14

$\{|{}|\}$ :

State to formula operator, Definition 21

${{{\varvec{\bigwedge }}}_{\,i j}\,}$ :

Static spatial modality, Definition 9

${{{\varvec{\bigwedge }}}_{\,i j}^{s}\,}$ :

Dynamic spatial modality, Definition 33

$AP _i$ :

The set of atomic propositions of process i, Sect. 2.1

$AP$ :

The set of all atomic propositions, Sect. 2.2

${{\upharpoonright }i}$ :

State projection onto process i, Definition 5 and  34

${{\upharpoonright } SH _{ij}}$ :

State projection onto the shared variables $SH _{ij}$, Definition 5

${{\upharpoonright }ij}$ :

State or path projection onto pair-program $(S_{ij}^0, P_{i}^{j}\!\parallel \!P_{j}^{i})$, Definitions 12 and 34

${{\upharpoonright }J}$ :

State or path projection onto a J-subprogram, Definitions 12, 18, 34, and 40

$\mathsf {PS}$ :

Pair-specification, Definition 3

$P_{i}^{j}$ :

Pair-process that represents process i in the pair-program consisting of processes i and j, Definition 4

$a_{i}^{j}$ :

Arc of process $P_{i}^{j}$, Sect. 5.3

$s_i, t_i$ :

Local state of process $P_{i}^{j}$ or process $P_{i}$, Sect. 2.1

$(S_{ij}^0, P_{i}^{j}\!\parallel \!P_{j}^{i})$ :

Pair-program consisting of processes i and j, Definition 4

$SH _{ij}$ :

Shared variables of $(S_{ij}^0, P_{i}^{j}\!\parallel \!P_{j}^{i})$, Definition 4

$S_{ij}^0$ :

The set of initial states of $(S_{ij}^0, P_{i}^{j}\!\parallel \!P_{j}^{i})$, Definition 4

$S_{ij}$ :

The set of states of $(S_{ij}^0, P_{i}^{j}\!\parallel \!P_{j}^{i})$, Definition 6

$R_{ij}$ :

The transition relation of $(S_{ij}^0, P_{i}^{j}\!\parallel \!P_{j}^{i})$, Definition 6

$M_{ij}$ :

Pair-structure of $(S_{ij}^0, P_{i}^{j}\!\parallel \!P_{j}^{i})$, Definition 6

$\mathscr {I}$ :

Global static specification, Definition 7

${\mathscr {I}}. pairs$ :

The pairs in $\mathscr {I}$, Definition 7

$I$ :

Interconnection relation, Definition 8

${ dom}(I)$ :

Domain of I, Definition 8

J :

Subrelation of I; gives a subprogram of $(S_I^0, P_{i_1}\!\parallel \!\ldots \!\parallel \!P_{i_K})$, Definition 11

${ dom}(J)$ :

Domain of J, Sect. 5.1

$(S_I^0, P_{i_1}\!\parallel \!\ldots \!\parallel \!P_{i_K})$ :

The global static program synthesized from $\mathscr {I}$, Definition 14

$P_{i}$ :

Process i in $(S_I^0, P_{i_1}\!\parallel \!\ldots \!\parallel \!P_{i_K})$, Definition 14

$a_{i}$ :

Arc in process $P_i$, Sect. 5.2

s :

I-state, Definition 11

$S_I^0$ :

The set of initial states of $(S_I^0, P_{i_1}\!\parallel \!\ldots \!\parallel \!P_{i_K})$, Definition 14

$S_I$ :

The set of states of $(S_I^0, P_{i_1}\!\parallel \!\ldots \!\parallel \!P_{i_K})$, Definition 15

$R_I$ :

The transition relation of $(S_I^0, P_{i_1}\!\parallel \!\ldots \!\parallel \!P_{i_K})$, Definition 15

$M_I$ :

I-structure of $(S_I^0, P_{i_1}\!\parallel \!\ldots \!\parallel \!P_{i_K})$, Definition 15

$W_I(s)$ :

The wait-for-graph for $(S_I^0, P_{i_1}\!\parallel \!\ldots \!\parallel \!P_{i_K})$ in I-state s, Definition 19

$\mathscr {D}$ :

Global dynamic specification, Definition 28

$\mathscr {PS}$ :

Universal set of pair-specifications, Definition 28

$\mathscr {PS}_0$ :

Initial set of pair-specifications, Definition 28

$\mathsf {create}$ :

Create mapping, Definition 28

${\mathscr {I}}. pairs$ :

The pairs in $\mathscr {I}$, Definition 7

s :

Configuration, Definition 31

$s.\mathscr {I}$ :

Pair-specifications in configuration s, Definition 31

$s.\mathcal{A}$ :

Pair-programs in configuration s, Definition 31

$s.\mathcal{S}$ :

State-mapping of configuration s, Definition 31

${s}.\textit{procs}$ :

Processes in configuration s, Definition 31

${s}. pairs$ :

Pairs in configuration s, Definition 31

$I _{s}$ :

Dynamic interconnection relation for configuration s, Definition 32

$\mathcal{P}$ :

The global dynamic program synthesized from $\mathscr {D}$, Definition 37

$P_i$ :

Process i in $\mathcal{P}$, Definition 37

$a_{i}$ :

Arc in process $P_i$, Sect. 7.2

$S^0$ :

The set of initial states of $\mathcal{P}$, Definition 37

S :

The set of states of $\mathcal{P}$, Definition 39

$R_n$ :

The normal transitions of $\mathcal{P}$, Definition 39

$R_c$ :

The create transitions of $\mathcal{P}$, Definition 39

$M_\mathcal{P}$ :

Structure (transition diagram) of $\mathcal{P}$, Definition 39

W(s):

The wait-for-graph for $\mathcal{P}$ in configuration s, Definition 42