Printer Friendly

Synthesis of current programs for an atomic read/write model of computation.

1. INTRODUCTION

Methods for synthesizing (finite state) concurrent programs from temporal logic specifications based on the use of a decision procedure for testing temporal satisfiability have been proposed by Emerson and Clarke [1982] and Manna and Wolper [1984]. An important advantage of these synthesis methods is that they obviate the need to manually compose a program and manually construct a proof of its correctness. One only has to formulate a precise problem specification; the synthesis method then mechanically constructs a correct solution. A serious drawback of these methods in practice, however, is that they produce concurrent programs for restricted models of parallel computation. For example, the method of Manna and Wolper [1984] produces CSP programs; in other words, programs with synchronous message passing. Moreover all communication takes place between a central synchronizing process and one of its satellite processes, and thus the overall architecture of such programs is highly centralized. The synthesis method of Emerson and Clarke [1982] produces concurrent programs for the shared-memory model of computation. Transitions of such programs are test-and-set operations in which a large number of shared variables can be tested and set in a single transition; in other words, the grain of atomicity is large. More recent synthesis methods [Anuchitanukul and Manna 1994; Pnueli and Rosner 1989a; 1989b] for synthesizing reactive modules assume that all of the inputs to a system can be consolidated into a single input variable [Pnueli and Rosner 1989a; 1989b], or into a global state that the module can read in one step [Anuchitanukul and Manna 1994]. In practice, the primitives provided by hardware are of small (and fixed) granularity, e.g., atomic read and write operations on a single register, or test-and-set operations on a single bit. It is therefore desirable to synthesize concurrent programs with small-grain operations.

In this paper, we present a method for synthesizing concurrent programs for a shared-memory model of computation in which the only operations are atomic reads or atomic writes of single variables. Our method accepts as input a formal specification, which can be expressed either as a finite-state machine, together with a temporal logic formula that specfies additional required properties (safety and liveness), or can be expressed just as a temporal logic formula. In the later case, the formula would be somewhat larger, since it must also express some "frame" properties such as the local structure of each process. From the specification, we first synthesize a correct program that, in general, contains test-and-set and multiple assignment operations. We then decompose these operations into sequences of atomic reads/writes. Finally, we modify the resulting program to ensure that it still satisfies the original specification, since new behaviors (that violate the specification) may have been introduced by the decomposition. We illustrate our method by synthesizing an atomic read/write solution to the mutual exclusion problem.

The paper is organized as follows. Section 2 presents our model of concurrent computation and our specification language. It also reviews the synthesis method of Emerson and Clarke [1982] and provides all the needed material from that earlier work. In particular, it discusses the relationship between programs and the globalstate transition diagrams that they give rise to (or, going in the other direction, can be "extracted" from). Section 3 formalizes our notion of concurrent programs in which the only operations are atomic reads or atomic writes of single variables. It also explores the relationship between these atomic read/write programs and the global-state transition diagrams from which such programs can be extracted. This lays the foundation for Section 4, which presents our synthesis method. Section 5 presents an example of the use of our method to synthesize an atomic read/write solution to the two-process mutual exclusion problem. Section 6 extends our method so that it produces programs for an atomic registers model. Section 7 analyzes the space complexity of our method. It then discusses related work, further directions for research, and concludes. Some of the longer proofs are omitted from the main body, and are provided in Appendix A; Appendix B provides a glossary of symbols.

2. PRELIMINARIES

2.1 Model of Concurrent Computation

We consider finite-state concurrent programs of the form P = [P.sub.1][parallel] ... [parallel][P.sub.K] that consist of a finite number of fixed sequential processes [P.sub.1], ...,[P.sub.K] running in parallel. With every process [P.sub.i], we associate a single, unique index, namely i. We observe that for most actual concurrent programs the portions of each process responsible for interprocess synchronization can be cleanly separated from the sequential applications-oriented computations performed by the process. This suggests that we focus our attention on synchronization skeletons which are abstractions of actual concurrent programs where detail irrelevant to synchronization is suppressed.

We may view the synchronization skeleton of an individual process [P.sub.i] as a state-machine where each state represents a region of code intended to perform some sequential computation and each arc represents a conditional transition (between different regions of sequential code) used to enforce synchronization constraints. For example, there may be a node labeled [C.sub.i] representing the critical section of process [P.sub.i]. While in [C.sub.i], the process [P.sub.i] may simply increment a single variable, or it may perform an extensive series of updates on a large database. In general, the internal structure and intended application of the regions of sequential code in an actual concurrent program are unspecified in the synchronization skeleton. By virtue of the abstraction to synchronization skeletons, we thus eliminate all steps of the sequential computation from consideration.

Formally, the synchronization skeleton of each process [P.sub.i] is a directed graph where each node is labeled by a unique name ([s.sub.i]) which represents a local state of [P.sub.i], and each arc is labeled with a synchronization command B [right arrow] A consisting of an enabling condition (i.e., guard) B and corresponding action A to be performed (i.e., a guarded command [Dijkstra 1976]). Each node must have at least one outgoing arc, i.e., a skeleton contains no "dead ends." A global state is a tuple of the form ([s.sub.1], ..., [s.sub.K], [v.sub.1], ..., [v.sub.m]) where each node [s.sub.i] is the current local state of [P.sub.i] and [v.sub.1], ..., [v.sub.m] is a list giving the current values of shared variables [x.sub.1], ..., [x.sub.m] (we assume that these are ordered in some fixed way, so that [v.sub.1], ..., [v.sub.m] specifies a unique value for each shared variable). A guard B is a predicate on states, and an action A is a parallel assignment statement that updates the values of the shared variables. If the guard B is omitted from a command it is interpreted as true, and we simply write the command as A. If the action A is omitted the shared variables are unaltered, and we write the command as B.

We model concurrency in the usual way by the nondeterministic interleaving of the "atomic" transitions of the individual synchronization skeletons of the processes [P.sub.i]. Hence, at each step of the computation, some process with an "enabled" arc is nondeterministically selected to be executed next. Assume that the current state is s = ([s.sub.1], ..., [s.sub.i], ..., [s.sub.K], [v.sub.1], ..., [v.sub.m]) and that process [P.sub.i] contains an arc from node [s.sub.i] to node [s'.sub.i] labeled by the command B [right arrow] A. If B is true in the current state then a permissible next state is ([s.sub.1], ..., [s'.sub.i], [s.sub.K], [v'.sub.1], ..., [v'.sub.m]) where [v'.sub.1], ..., [v'.sub.m] is the list of updated values for the shared variables resulting from the execution of action A. The arc from [s.sub.i] to [s'.sub.i] is said to be enabled in state s. An arc that is not enabled is disabled, or blocked. A computation path is any sequence of states where each successive pair of states is related by the above next-state relation. Note that the operations involved in just checking the value of a guard B are not explicitly represented by the next-state relation given above. In particular, if B is checked and found to be false, then no change occurs, not even an indication that some computation has occurred at a "lower" implementation level. Essentially, when [P.sub.i] is in some local state [s.sub.i], the guards of all the arcs leaving [s.sub.i] must be repeatedly checked until one of them is found to be true, at which point [P.sub.i] can execute the corresponding arc. Thus, guards really hide "busy wait" loops (or "await" primitives) where their value is checked. We discuss these issues further in Section 6.

The synthesis task thus amounts to supplying the commands to label the arcs of each process' synchronization skeleton so that the resulting global-state transition diagram of the entire program [P.sub.1][parallel] ... [parallel][P.sub.K] meets a given temporal logic specification.

2.2 Programs and Global-State Transition Diagrams

We consider the semantics of a program P to be given by the global state transition diagram M that is generated by all the computation paths of P starting from a specified set of initial states [S.sub.0]. We now formalize our notions of program and global-state transition diagram.

Definition 2.2.1 (Program). A program P = [P.sub.1][parallel] ... [parallel][P.sub.K] is the parallel composition of K processes [P.sub.1], ..., [P.sub.K]. Associated with each process [P.sub.i] is a set of atomic propositions A[P.sub.i] (with A[P.sub.i] [union] A[P.sub.j] = 0 when i [not equal to] j). Let AP = [[union].sub.i[member of][1:K]] A[P.sub.i]. (1) Each process [P.sub.i] is a synchronization skeleton. An arc of [P.sub.i] (henceforth called a [P.sub.i]-arc) is a tuple ([s.sub.i], B [right arrow] A, [t.sub.i]), where [s.sub.i], [t.sub.i] are local states of [P.sub.i] (henceforth called [P.sub.i]-states), and B [right arrow] A is an arc label, consisting of a [P.sub.i]-guard B and a multiple assignment statement A. B is built up from the standard propositional logic connectives, the atomic propositions in AP - A[P.sub.i], and expressions of the form x = c (c [member of] [D.sub.x]), where x is a shared variable in P, and c is some value drawn from [D.sub.x], the domain of x. A multiple assignment statement has the form [//.sub.m[member of][1:n]] [x.sup.m] := [c.sup.m] where [x.sup.m] is a shared variable in P, and [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII], for all m [member of] [1 : n]. (2) Associated with each [P.sub.i]-state [s.sub.i] is a local atomic proposition valuation L[[s.sub.i]] [subset or equal to] A[P.sub.i]. L[[s.sub.i]] contains the atomic propositions that are true in [s.sub.i]. Also, all of the structures defined here are finite, since our programs are finite-state.

We shall use the term "local state" when we intend to say [P.sub.i]-state for some unspecified process index i. Let SH denote the set of all shared variables in P, and let A denote the set of all multiple assignment statements in P.

We shall find it technically convenient in the sequel to "group" the atomic propositions in A[P.sub.i] into a single variable [L.sub.i] whose value in [s.sub.i] is L[[s.sub.i]]. We also extend the definition of i-state to provide for a value assigned to [L.sub.i] by every i-state. [L.sub.i] may be regarded as a concrete implementation of the atomic propositions in A[P.sub.i]. For a particular i-state [s.sub.i], the corresponding value of [L.sub.i] is given by

(LOC) [s.sub.i]([L.sub.i]) = L[[s.sub.i]],

i.e., [L.sub.i] is the set of atomic propositions in A[P.sub.i] that are true in i-state [s.sub.i]. In practice, [L.sub.i] could be encoded efficiently as a bit string. Since the atomic propositions of [P.sub.i] (those in A[P.sub.i]) can be read by other processes, and since the value of the atomic propositions of [P.sub.i] gives some information about the possible current local state of [P.sub.i], we shall refer to [L.sub.i] as the externally visible location counter of [P.sub.i]. However, it is possible for different local states of [P.sub.i] to have the same local atomic proposition valuation, and thus the same value of [L.sub.i]. Hence [L.sub.i] does not uniquely determine the current local state of [P.sub.i]. Thus, the actual location counter of [P.sub.i] is properly thought of as having two components: the externally visible [L.sub.i], and an internal component (not readable by processes other than [P.sub.i]) that distinguishes between local states of [P.sub.i] that happen to have the same local atomic proposition valuation. This internal component is formalized in Section 3.2 below. The presence of this internal component allows [P.sub.i] to change its local state without executing a write operation to a variable that other processes can read (namely [L.sub.i]). If every transition of [P.sub.i] required a write operation to [L.sub.i], then [P.sub.i] could never read the value of a shared variable (or the [L.sub.j] of some other process [P.sub.j]) without violating the requirements of the atomic read/write model. Thus, the decomposition of the location counter into an externally visible component and an internal component facilitates the introduction of "read only" transitions during the refinement of the initial high-atomicity program into an atomic read/write program.

If s = ([s.sub.1, ..., [s.sub.i], ..., [s.sub.K], [v.sub.1], ..., [v.sub.m]) is a global state, then we define s [up arrow] i = [s.sub.i] and s [up arrow] SH = ([v.sub.1], ..., [v.sub.m]). (3) We write [s.sub.i]([Q.sub.i]), s([Q.sub.i]) for the value of atomic proposition [Q.sub.i] in local state [s.sub.i], global state s respectively. [s.sub.i]([Q.sub.i]) = true if [Q.sub.i] [member of] L[[s.sub.i]], and false otherwise, [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII].

Definition 2.2.2 (Global-State Transition Diagram). The global-state transition diagram of program P = [P.sub.1][parallel] ... [parallel][P.sub.K] is a tuple ([S.sub.0], S, R) where

(1) S is the set of all global states of [P.sub.1][parallel] ... [parallel][P.sub.K], and

(2) So [subset or equal to] S is the set of initial states of [P.sub.1][parallel] ... [parallel][P.sub.K], and

(3) R [subset or equal to] S x [1: K] x A x S is the set of transitions of [P.sub.1][parallel] ... [parallel][P.sub.K], that is, the set of all transitions [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] such that

(a) i [member of] [1 : K], and

(b) s [member of] S, t [member of] S (i.e., s and t are global states of [P.sub.1][parallel] ... [parallel][P.sub.K]), and

(c) [conjunction]j [member of] [1 : K] - {i} : s [up arrow] j = t [up arrow] j, and

(d) there exists an arc (s [up arrow] i, B [right arrow] A, t [up arrow] i) in [P.sub.i] such that

i. s(B) = true, (4) and

ii. <(s [up arrow] SH> A <t [up arrow] SH>.

<s [up arrow] SH> A <t [up arrow] SH> is Hoare triple notation [Hoare 1969] for total correctness, which in this case means that execution of A always terminates, (5) and, when the shared variables in SH have the values assigned by s, leaves these variables with the values assigned by t. Note that whenever we say "state" we intend "global state," unless the context makes it clear that a local state is intended. A transition by [P.sub.i] (i.e., of the form [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]) is referred to as a [P.sub.i]-transition. A (computation) path is therefore a sequence of transitions such that the end state of each transition is the start state of the next transition. An initialized path is a path that starts in an initial state. A state is reachable iff it lies on some initialized path. A transition is reachable iff its source state is reachable. If all transitions in a global-state transition diagram are reachable, then we say that the global-state transition diagram is in reachable form.

Figure 1 gives an example program P = [P.sub.1][parallel][P.sub.2] together with the global-state transition diagram M generated by applying Definition 2.2.2 to P. The atomic propositions are {[D.sub.1], [E.sub.1]} for process [P.sub.1], and {[D.sub.2], [E.sub.2]} for process [P.sub.2]. The initialstate set is {[s.sup.0]}. In each global (local) state, we display the propositions that are true.

[FIGURE 1 OMITTED]

2.3 The Temporal Logic CTL

CTL [Emerson and Clarke 1982; Emerson 1990] is a propositional branching time temporal logic. We have the following syntax for CTL, where [Q.sub.i] denotes an atomic proposition in A[P.sub.i], i [member of] [1 : K], and f, g denote (sub-)formulae.

(1) Each of [Q.sub.i], f [conjunction] g, and [logical not] f is a formula (where the latter two constructs indicate conjunction and negation, respectively).

(2) E[X.sub.j]f is a formula which means that there is an immediate successor state reachable by executing one arc of process [P.sub.1], j [member of] [1: K], in which formula f holds.

(3) A[f [union] g] is a formula which means that for every maximal computation path there is some state along the path where g holds, and f holds at every state along the path until that state.

(4) E[f [union] g] is a formula which means that for some maximal computation path there is some state along the path where g holds, and f holds at every state along the path until that state.

Formally, we define the semantics of CTL formulae with respect to a Kripke structure M = ([S.sub.0], S, R) consisting of
S, a countable set of global states.
[S.sub.0] [subset or equal to] S, a countable set of initial states.
R [subset or equal to] S x [1 : K] x A x S, a transition relation. R
  is partitioned into relations [R.sub.1], ..., [R.sub.K], where
  [R.sub.i] gives the transitions of process i.


A fullpath is a maximal computation path, i.e., a path that is either infinite or ends in a state with no outgoing transitions. If [pi] is a fullpath, then define |[pi]|, the length of [pi], to be [omega] when [pi] is infinite and k when [pi] is finite and of the form ([s.sup.0], ..., [s.sub.k]). We use the usual notation for truth in a structure: M, [s.sup.0] [satisfies] f means that f is true at state [s.sup.0] in structure M. When the structure M is understood, we write [s.sup.0] [satisfies] f. We define [satisfies] inductively:
M, [s.sup.0] [satisfies] [Q.sub.i] iff [Q.sub.i] [member of]
  L[[s.sup.0] [up arrow] i]

M, [s.sup.0] [satisfies] [logical not] f iff not(M,
  [s.sup.0] [satisfies] f)

M, [s.sup.0] [satisfies] f [conjunction] g iff M, [s.sup.0]
  [satisfies] f and M, [s.sup.0] [satisfies] g

M, [s.sup.0] [satisfies] E[X.sub.j] f iff for some state t,
  ([s.sup.0],t) [member of] [R.sub.j] and M, t [satisfies] f

M, [s.sup.0] [satisfies] A[f [union] g] iff for all
  fullpaths [pi] = ([s.sup.0], [s.sup.1], ...) in M that start in
  [s.sup.0], there exists i [member of] [0 : |[pi]|] such that
  M, [s.sup.i] [satisfies] g and for all j [member of] [1 : (i - 1]:
  M, [s.sup.j] [satisfies] f

M, [s.sup.0] [satisfies] E[f [union] g] iff some fullpath
  [pi] = ([s.sup.0], [s.sup.1], ...) in M that start in
  [s.sup.0], there exists i [member of] [0 : |[pi]|] such that
  M, [s.sup.i] [satisfies] g and for all j [member of] [1 : (i - 1]:
  M, [s.sup.j] [satisfies] f


We say that a formula f is satisfiable if and only if there exists a structure M and state s of M such that M, s [satisfies] f. In this case, we say that M is a model of f. We say that a formula f is valid if and only if M, s [satisfies] f for all structures M and states s of M.

We use the notation M, U [satisfies] f as an abbreviation of [for all]s [member of] U : M, s [satisfies] f, where U [subset or equal to] S. We introduce the abbreviations f [disjunction] g for [logical not]([logical not] f [conjunction] [logical not] g), f [??] g for [logical not] f [disjunction] g, f [equivalent to] g for (f [??] g) [conjunction] (g [??] f), AFf for A[true [union] f], EFf for E[true [union] f, AGf for [logical not] EF [logical not] f, EGf for [logical not] AF [logical not]] f, A[Y.sub.i]f for [logical not] E[X.sub.i] [logical not] f, EXf for E[X.sub.1] f [disjunction] ... [disjunction] E[X.sub.k]f, and AYf for A[Y.sub.1]f [conjunction] ... [conjunction] A[Y.sub.k] f.

A formula of the form A[f [union] g] or E[f [union] g] is an eventuality formula. An eventuality corresponds to a liveness property in that it makes a promise that something does happen. This promise must be fulfilled. The eventuality A[f [union] g] (E[f [union] g]) is fulfilled for s in M provided that for every (respectively, for some) path starting at s, there exists a finite prefix of the path in M whose last state satisfies g and all of whose other states satisfy f. Since AFg and EFg are special cases of A[[f [union] g]] and E[[f [union] g]], respectively, they are also eventualities. In contrast, AGf and EGf are invariance formulae. An invariance corresponds to a safety property, since it asserts that whatever happens to occur (if anything) will meet certain conditions.

Following Definition 2.2.2, we annotate transitions in a Kripke structure with the index i of the process executing the transition, and the assignment statement A (if any) that [P.sub.i] executes, e.g., [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]. In the sequel, we assume, for all Kripke structures M = ([S.sub.0], S, R), and all [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] and <s [up arrow] SH> A <t [up arrow] SH>. This merely excludes Kripke structures that do not respect our model of concurrent computation. All Kripke structures generated by our synthesis method (and the method of Emerson and Clarke [1982]) satisfy this assumption.

2.4 The Specification Language

For the purposes of this paper, we restrict specifications to the sublogic of CTL whose formulae are finite conjunctions of the following terms:

--h, where h [member of] LO(AP, [logical not], [conjunction]), specifies the initial states. (6)

--AGh, where h [member of] LO(AP, [logical not], [conjunction]), specifies safety properties, since AGh is satisfied by all initial states iff h is satisfied by all reachable states, i.e., h is invariant.

--AG(p [??] A[q [union] r]), where p,q,r [member of] LO(AP, [logical not], [conjunction]), specifies a temporal leads-to property, combined with an "unless" property: from any global state satisfying p, eventually a state satisfying r must be reached (along all outgoing fullpaths), and all intervening states must satisfy q.

--AG([p.sub.i] [??] E[X.sub.i][q.sub.i]), where [p.sub.i], [q.sub.i] [member of] LO(A[P.sub.i], [logical not], [conjunction]), specifies a local structure property; from every reachable state satisfying [p.sub.i], there exists an outgoing [P.sub.i]-transition to a state satisfying [q.sub.i]. In the synthesized program, such a transition (if it involves both a test and a set) will be broken down into a test transition followed by some set transitions. Hence, the synthesized program will not, in general, satisfy AG([p.sub.i] [??] E[X.sub.i][q.sub.i]); it will, however, satisfy AG([p.sub.i] [??] E[X.sub.i]([p.sub.i] [disjunction] [q.sub.i])). For technical reasons, we require [p.sub.i] [not equivalent to] [q.sub.i].

--AG([p.sub.i] [??] A[Y.sub.i][q.sub.i]), where [p.sub.i], [q.sub.i] [member of] LO(A[P.sub.i], [logical not], [conjunction]), specifies a local structure property; from every reachable state satisfying [p.sub.i], every outgoing [P.sub.i]-transition is to a state satisfying [q.sub.i]. For the same reason as given for AG([p.sub.i] [??] E[X.sub.i][q.sub.i]), the synthesized program will not, in general, satisfy AG([p.sub.i] [??] A[Y.sub.i][q.sub.i]); it will, however, satisfy AG([p.sub.i] [??] A[Y.sub.i]([p.sub.i] [disjunction] [q.sub.i])).

In addition, we assume that AGEXtrue is always a conjunct of the specification. That is, we restrict our attention to nonterminating concurrent programs.

An example specification is given below for the two-process mutual exclusion problem. In this specification, process [P.sub.i], i [member of] {1, 2}, is always in exactly one of three states [N.sub.i], [T.sub.i], [C.sub.i], which represent, respectively, the noncritical, trying, and critical code regions. A process in its noncritical state does not require the use of critical (shared) resources, and performs computations that can proceed in parallel with computations by the other processes. A process requiring a critical resource moves into the trying state. From there, it enters the critical state as soon as possible, provided that all constraints on the use of the critical resource are met. In the critical state, [P.sub.i] has access to the critical resource. This specification is given by the following set of CTL formulae (which are implicitly conjoined):

(1) Initial State (both processes are initially in their noncritical region):

[N.sub.1] [conjunction] [N.sub.2]

(2) It is always the case that any move [P.sub.1] makes from its noncritical region is into its trying region and such a move is always possible. Likewise for [P.sub.2]:

AG([N.sub.1] [??] (A[Y.sub.1][T.sub.1] [conjunction] E[X.sub.1][T.sub.1])) AG([N.sub.2] [??] (A[Y.sub.2][T.sub.2] [conjunction] E[X.sub.2][T.sub.2]))

(3) It is always the case that any move [P.sub.1] makes from its trying region is into its critical region. Likewise for [P.sub.2]:

AG([T.sub.1] [??] (A[Y.sub.1][C.sub.1])) AG([T.sub.2] [??] (A[Y.sub.2][C.sub.2]))

(4) It is always the case that any move [P.sub.1] makes from its critical region is into its noncritical region and such a move is always possible. Likewise for [P.sub.2]:

AG(C1 [??] (A[Y.sub.1][N.sub.1] [conjunction] E[X.sub.1][N.sub.1])) AG(C2 [??] (A[Y.sub.2][N.sub.2] [conjunction] E[X.sub.2][N.sub.2]))

(5) [P.sub.1] is always in exactly one of the states [N.sub.1], [T.sub.1], or [C.sub.1]. Likewise for [P.sub.2]:

AG([N.sub.1] [equivalent to] [logical not]([T.sub.1] [disjunction] [C.sub.1])) [conjunction] AG([T.sub.1] [equivalent to] [logical not]([N.sub.1] [disjunction] [C.sub.1])) [conjunction] AG([C.sub.1] [equivalent to] [logical not]([N.sub.1] [disjunction] [T.sub.1]))

AG([N.sub.2] [equivalent to] [logical not]([T.sub.2] [disjunction] [C.sub.2])) [conjunction] AG([T.sub.2] [equivalent to] [logical not]([N.sub.2] [disjunction] [C.sub.2])) [conjunction] AG([C.sub.2] [equivalent to] [logical not]([N.sub.2] [disjunction] [T.sub.2]))

(6) Every request for critical section entry by [P.sub.1], [P.sub.2] is eventually granted, i.e., [P.sub.1], [P.sub.2] do not starve:

AG([T.sub.1] [??] AF[C.sub.1]) AG([T.sub.2] [??] AF[C.sub.2])

(7) A transition by one process cannot cause a transition by another (interleaving model of concurrency):

AG(([N.sub.1] [??] A[Y.sub.2][N.sub.1]) [conjunction] ([N.sub.2] [??] A[Y.sub.1][N.sub.2])) AG(([T.sub.1] [??] A[Y.sub.2][T.sub.1]) [conjunction] ([T.sub.2] [??] A[Y.sub.1][T.sub.2])) AG(([C.sub.1] [??] A[Y.sub.2][C.sub.1]) [conjunction] ([C.sub.2] [??] A[Y.sub.1][C.sub.2]))

(8) [P.sub.1], [P.sub.2] do not access critical resources together:

AG([logical not]([C.sub.1] [conjunction] [C.sub.2]))

(9) It is always the case that some process can move:

AGEXtrue

Note that since AF f [equivalent to] A[true [union] f], the above is within our specification language.

2.5 Correctness Properties of Programs

Let M = ([S.sub.0], S, R) be the global-state transition diagram of program P. From the definitions of global-state transition diagram and Kripke structure given above, we see that M can be considered to be a Kripke structure. Hence, we consider a program P to be correct with respect to a specification f (expressed as a CTL formula) iff M, [S.sub.0] [satisfies] f. In other words, the specification must be true in all the initial states of the global-state transition diagram of the program. In this case, we say that program P satisfies specification f.

2.6 Synthesis of Programs

Our method builds on and extends the synthesis method of Emerson and Clarke [1982]. (7) The method of Emerson and Clarke [1982] starts with a CTL specification f and applies a tableau-based decision procedure to f. If f is satisfiable, the decision procedure constructs a tableau from which a model M of f can be constructed. For example, Figure 2 shows the model generated for the two-process mutual exclusion specification given in Section 2.4. The model M can be regarded as the global-state transition diagram of a correct program, and this program can be extracted from M by "projecting" onto the individual processes. This extraction operation was described informally in Emerson and Clarke [1982]. To establish our technical results, we need a formal definition of program extraction. We proceed as follows.

[FIGURE 2 OMITTED]

Let s be a state. We use s [down arrow] i for s - {[s.sub.i]}, i.e., s with its [P.sub.i]-component removed. We define,

Definition 2.1 (State-to-Formula Definition).

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

where Q ranges over AP

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

where Q ranges over AP - A[P.sub.i]

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

where Q ranges over A[P.sub.i].

{s} characterizes s in that s [satisfies] {s}, and s' [??] {s} for all states s' such that s' [not equal to] s, i.e., it converts a state into a propositional formula. For example, {[s.sup.0]} = [A.sub.1] [conjunction] [logical not][B.sub.1] [conjunction] [A.sub.2] [conjunction] [logical not][B.sub.2], where [s.sup.0] is the global state depicted in Figure 1.

From the global-state transition diagram definition (2.2.2), we see that a particular [P.sub.i]-arc ([s.sub.i], B [right arrow] A, [t.sub.i]) generates a set of [P.sub.i]-transitions; it generates one [P.sub.i]-transition in every state s such that s [up arrow] i = [s.sub.i] and s(B) = true. We group all the [P.sub.i]-transitions generated by a single [P.sub.i]-arc into a [P.sub.i]-family: (8)

Definition 2.2 ([P.sub.i]-Family). A [P.sub.i]-family F in a Kripke structure M = ([S.sub.0], S, R) is a maximal subset of R such that

(1) all members of F are [P.sub.i]-transitions, and have the same label [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII], and

(2) for any pair [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII], [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] of members of F: s [up arrow] i = s' [up arrow] i and t [up arrow] i = t' [up arrow] i.

If [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII], then let F.start, F.finish, F.assig, F.label denote s [up arrow] i, t [up arrow] i, A, and [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] respectively. Given that T.begin denotes the source state of transition T, i.e., T.begin = s for transition [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII], let F.guard denote [[disjunction].sub.T[member of]F]{(T.begin) [down arrow] i}.

When [P.sub.i] is understood from context, or when we wish to refer to a [P.sub.i]-family for an unspecified [P.sub.i], we will use the term "family," i.e., we drop the prefix "[P.sub.i]-". F.guard is equivalent to the guard B of the [P.sub.i]-arc (s [up arrow] i, B [right arrow] A, t [up arrow] i) which generates F. (9) The [P.sub.i]-family definition allows us to give a succinct definition for the operation of extracting a program from a Kripke structure. This definition formalizes the extraction technique of Emerson and Clarke [1982].

Definition 2.3 (Program Extraction Definition). Let M = ([S.sub.0], S, R) be an arbitrary Kripke structure. Then the program P = [P.sub.1][parallel] ... [parallel][P.sub.K] extracted from M is given by

([s.sub.i], B [right arrow] A, [t.sub.i]) [member of] [P.sub.i] iff there exists a [P.sub.i]-family F in M such that F.start = [s.sub.i], F.finish = [t.sub.i], F.assig = A, F.guard = B.

For example, the Kripke structure shown in Figure 2 contains the [P.sub.1]-families

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII],

and the [P.sub.2] families

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII],

Applying Definition 2.3, the above families give rise to the following [P.sub.1]-arcs, respectively

([N.sub.1], [N.sub.2] [disjunction] [C.sub.2] [right arrow] skip, [T.sub.1]),

([N.sub.1], [T.sub.2] [right arrow] x := 2, [T.sub.1]),

([T.sub.1], [N.sub.2] [disjunction] ([T.sub.2] [conjunction] x = 1) [right arrow] skip, [C.sub.1]),

([C.sub.1], [N.sub.2] [disjunction] [T.sub.2] [right arrow] skip, [N.sub.1]),

and the following [P.sub.2]-arcs, respectively,

([N.sub.2], [N.sub.1] [disjunction] [C.sub.1] [right arrow] skip, [T.sub.2]),

([N.sub.2], [T.sub.1] [right arrow] x := 1, [T.sub.2]),

([T.sub.2], [N.sub.1] [disjunction] ([T.sub.1] [conjunction] x = 2) [right arrow] skip, [C.sub.2]),

([C.sub.2], [N.sub.1] [disjunction] [T.sub.1] [right arrow] skip, [N.sub.2]).

The resulting program is depicted in Figure 3. We remark that this program contains large-grain atomicity operations. For example, one of the arcs from [N.sub.1] to [T.sub.1] is labeled with the guarded command [T.sub.2] [right arrow] x := 2. Thus the atomic proposition [T.sub.2] must be tested, and then the assignment x := 2 must be performed. In addition, the values assigned to the atomic propositions [N.sub.1], [T.sub.1] must be changed from true, false respectively to false, true respectively. So, overall, a test followed by a multiple assignment must be performed as a single atomic operation.

[FIGURE 3 OMITTED]

Definition 2.3 guarantees that the execution of program P generates the same structure M that P was extracted from, i.e., the program extraction and global-state transition diagram generation operations are "inverses." In particular, the use of F.guard = [[disjunction].sub.T [member of] F]{(T.begin) [down arrow] i} as the guard B of the arc ([s.sub.i], B [right arrow] A, [t.sub.i]) corresponding to family F ensures that all and only the transitions in F are generated by the execution of ([s.sub.i], B [right arrow] A, [t.sub.i]). When [P.sub.i] is in state [s.sub.i], the disjunct {(T.begin) [down arrow] i} of F.guard evaluates to true if and only if the current global state is T.begin. Hence, {(T.begin) [down arrow] i} contributes the transition T (and only the transition T) to the global-state transition diagram of P. Hence, F.guard contributes exactly the transitions in F, as desired.

We note that the model in Figure 2 contains a shared variable x. This variable serves to disambiguate the states [[T.sub.1] x = 1 [T.sub.2]] and [[T.sub.1] x = 2 [T.sub.2]], which are propositionally equivalent, but differ temporally, since [[T.sub.1] x = 1 [T.sub.2]] satisfies E[X.sub.1]true, while [[T.sub.1] x = 2 [T.sub.2]] satisfies E[X.sub.2]true. Without x, the extracted program would generate a global-state transition diagram in which these states are "merged" into a single global state [[T.sub.1] [T.sub.2]]. This is because the extracted program depends only on the propositional component of the states, and does not take the temporal information that labels the states into account (see Emerson and Clarke [1982]). In this global-state transition diagram, there is a cycle [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]. This cycle causes violation of the absence-of-starvation specification AG([T.sub.2] [??] AF[C.sub.2]). Hence we see that it is necessary that propositionally identical states be disambiguated in some way, e.g., by the use of shared variables.

In summary, we see that there is a correspondence between [P.sub.i]-arcs in a program P and [P.sub.i]-families in the global-state transition diagram M of P. A [P.sub.i]-arc A[R.sub.i] in P gives rise to a [P.sub.i]-family of transitions in M which represent all the possible executions of A[R.sub.i], i.e., the executions of A[R.sub.i] in all the global states that satisfy the guard of A[R.sub.i], and where local control of [P.sub.i] is "at" the start state of A[R.sub.i], as specified by the global-state transition diagram definition (2.2.2). Also, a [P.sub.i]-family F of transitions in M gives rise to a single [P.sub.i]-arc when P is extracted from M, the guard of this arc being the disjunction of all global states s (with the [P.sub.i]-component removed, i.e., s [down arrow] i, and then converted to a formula, i.e., {s [down arrow] i}) which are source states of some transition in F.

3. ATOMIC READ/WRITE SYNTAX AND SEMANTICS

3.1 Syntactic Characterization of Atomic Read/Write Programs

We recall that a [P.sub.i]-transition of a program P = [P.sub.1][parallel] ... [parallel][P.sub.K] may, in general, change one or more atomic propositions in A[P.sub.i] and/or shared variables. In effect, the [P.sub.i]-transition executes a multiple assignment. Since we aim to synthesize programs for an atomic read/write model of computation, such a [P.sub.i]-transition must be decomposed into a series of [P.sub.i]-transitions, each of which executes a single assignment.

Intuitively, P = [P.sub.1][parallel] ... [parallel][P.sub.K] is an atomic read/write program iff the execution of every arc (of every process of) P requires only a single atomic read operation or a single atomic write operation. We formalize this by defining a set of syntactic arc attributes (Definition 3.1.2 below). These attributes characterize an arc in terms of the atomic read/write operations that are required to implement it. Some of the clauses of Definition 3.1.2 have an accompanying (indented) paragraph of explanatory text.

Definition 3.1.1 (Syntactic Equality). We use [??] to denote syntactic equality. i.e., B [??] true means that B is the constant true. If B is [N.sub.1] [disjunction] [logical not][N.sub.1], for example, then B [??] true.

Definition 3.1.2 (Syntactic Arc Attributes). We define the following seven attributes of synchronization skeleton arcs.

--An arc ([s.sub.i], B [right arrow] A, [t.sub.i]) is guarded iff B [??] true. A guarded arc requires one or more read operations for its implementation, since the guard, in general, refers to shared variables and/or atomic propositions (of other processes), which must be read in order that the guard be evaluated.

--An arc ([s.sub.i], B [right arrow] A, [t.sub.i]) is unguarded iff B [??] true. An unguarded arc requires no read operations for its implementation, since it can be executed unconditionally when local control is "at" its start state.

--An arc ([s.sub.i], B [right arrow] A, [t.sub.i]) is single-writing iff A [??] skip and L[[s.sub.i]] [not equal to] L[[t.sub.i]], or A [??] "x := c" (for some shared variable x and c [member of] [D.sub.x]) and L[[s.sub.i]] = L[[t.sub.i]]. In the first case, a single write operation is needed to set the values of all atomic propositions in A[P.sub.i] to those assigned by [t.sub.i]. Since these atomic propositions are combined into the externally visible location counter [L.sub.i], this requires only a single write operation. In the second case, a single write operation sets the shared variable x to the constant c.

--An arc ([s.sub.i], B [right arrow] [//.sub.m[member of][1:n]] [x.sup.m] := [c.sup.m], [t.sub.i]) is multiple-writing iff n > 1, or (n > 0 and L[[s.sub.i]] [not equal to] L[[t.sub.i]]). In the first case, one write operation is needed to set the values of all atomic propositions in A[P.sub.i] to those assigned by [t.sub.i], and at least one write operation is needed to perform [//.sub.m[member of][1:n]] [x.sup.m] := [c.sup.m], since we have n > 0. In the second case, n > 1 write operations are needed to perform [//.sub.m[member of][1:n]] [x.sup.m] := [c.sup.m]. Note that an arc ([s.sub.i], B [right arrow] skip, [t.sub.i]) is never multiple-writing.

--An arc is writing iff it is either single-writing or multiple-writing.

--An arc ([s.sub.i], B [right arrow] skip, [t.sub.i]) is nonwriting iff L[[s.sub.i]] = L[[t.sub.i]]. An arc is nonwriting if and only if it is not writing.

--An arc is test-and-set iff it is both guarded and writing.

Define a simple term to be a formula of the form [Q.sub.i] [member of] [L.sub.i], (where [Q.sub.i] [member of] A[P.sub.i], i [member of] [1 : K]), or of the form x = c, (where x [member of] SH, c [member of] [D.sub.x]). In an atomic read/write model, a simple term can be used as the guard of an arc, since checking that a simple term evaluates to true (and therefore that the arc can be executed) can be done using a single atomic read operation (which reads the single shared variable or externally visible location counter that the simple term refers to, depending on its form). Likewise, a disjunction of simple terms can be used as the guard of an arc, since checking that a disjunction evaluates to true reduces to checking that one of its disjuncts evaluates to true. However, a conjunction of terms (simple or otherwise) cannot be used as the guard of an arc in a straightforward manner, since checking that a conjunction evaluates to true requires us to check that all conjuncts evaluate to true simultaneously. This requires the simultaneous reading of all the shared variables and location counters that are mentioned in any conjunct, and the atomic read/write model does not permit such "multiple" reads.

Definition 3.1.3 (Single-Reading). An arc ([s.sub.i], B [right arrow] A, [t.sub.i]) is single-reading iff B is a disjunction of simple terms.

Note, that in the synchronization skeleton model, [P.sub.i] does not need to read its own local state [s.sub.i], since the model requires that local control of [P.sub.i] is "at" [s.sub.i] before ([s.sub.i], B [right arrow] A, [t.sub.i]) can be executed. (In Section 6, we show how to translate our synchronization skeleton programs into a model based on atomic read/write registers. In this model, the local state [s.sub.i] does have to be read by process [P.sub.i].)

Definition 3.1.4 (Atomic Read/Write Program). P is an atomic read/write program iff P is a program such that every arc in P is either single-reading and nonwriting, or unguarded and single-writing.

3.2 Numbered Local States

By Definition 3.1.4 above, P = [P.sub.1][parallel] ... [parallel][P.sub.K] is in atomic read/write form iff every arc of every process [P.sub.1], ..., [P.sub.K] either reads a single variable or writes a single variable. In our framework, there are two types of variables: (1) shared variables, which every process can read/write, and (2) the externally visible location counter, which the owning process can write and which every other process can read. Consider an arc of [P.sub.i] that reads a single variable. This arc must have the form ([s.sub.i], B [right arrow] skip, [t.sub.i]), where B references the variable. Also, L[[s.sub.i]] = L[[t.sub.i]], since no atomic propositions in A[P.sub.i] can be modified. However, it is clear that, in general, [s.sub.i] and [t.sub.i] do not denote the same i-state (i.e., [s.sub.i] [not equal to] [t.sub.i]), since [P.sub.i] makes the transition from [s.sub.i] to [t.sub.i] based on B evaluating to true. If [s.sub.i] and [t.sub.i] were the same i-state, then executing the arc ([s.sub.i], B [right arrow] skip, [t.sub.i]) would not change anything, i.e., there would be no point in testing the truth of B, since the final local state is the same regardless of the outcome of the test. Thus, the value read has no effect on subsequent execution. (10) We conclude that in general [s.sub.i] and [t.sub.i] are different i-states that happen to assign the same truth values to all atomic propositions in A[P.sub.i], and therefore have the same externally visible location counter. Now, when the current i-state is [t.sub.i] instead of [s.sub.i], this records the fact that B evaluated to true. Hence, the read operation impacts the subsequent execution.

Since the externally visible location counter does not distinguish [s.sub.i] and [t.sub.i], we introduce a function num, from the set of i-states to the natural numbers, that assigns a natural number to each i-state. The idea is that i-states with the same externally visible location counter (i.e., local atomic proposition valuations) are assigned different numbers:

(NUM) L[[s.sub.i]] = L[[t.sub.i]] [conjunction] [s.sub.i] [not equal to] [t.sub.i] [??] num([s.sub.i]) [not equal to] num([t.sub.i]).

Since another way of writing (NUM) is

L[[s.sub.i]] = L[[t.sub.i]] [conjunction] num([s.sub.i]) = num([t.sub.i]) [??] [s.sub.i] = [t.sub.i],

we can take the pair (L[[s.sub.i]], num[s.sub.i])) as uniquely defining [s.sub.i], i.e., as giving the location counter (which, in effect, points to the "current" local state). L[[s.sub.i]] is the externally visible component of the location counter (readable by other processes), and num([s.sub.i]) is the internal component of the location counter (not readable by other processes). In examples, we shall not give local states explicit names (e.g., [s.sub.i], [t.sub.i], etc.) but will use the combination of L[[s.sub.i]] and num([s.sub.i]) to identify local states. We shall usually indicate the number assigned to an i-state as a superscript, e.g., [s.sup.1.sub.i], [s.sup.2.sub.i], etc. Since a global state is a tuple of local states and shared variable values, we shall not name global states in examples. Global states are uniquely identified by their constituent local states and shared variable values.

3.3 Atomic Read/Write Kripke Structures

In Sections 2.2 and 2.6, we dealt with the relationship between programs and Kripke structures. Since an arbitrary Kripke structure can contain transitions that assign to several shared variables and test the global state, it is clear that the programs extracted from such a structure must contain "test-and-set" operations of a large grain of atomicity. Since the set of all (finite state) programs corresponds (via extraction in one direction and global-state transition diagram generation in the other) to the set of all (finite state) Kripke structures, it follows from the above that the set of atomic read/write programs corresponds to a proper subset of the set of (finite state) Kripke structures. We now define this subset: the atomic read/write Kripke structures. We also define the operation for extracting an atomic read/write program from an atomic read/write Kripke structure.

Since there is a correspondence between [P.sub.i]-arcs and [P.sub.i]-families, the syntactic arc attributes can be extended to families merely by applying Definition 3.1.2 to the arc corresponding to the family. We do this for the "writing" attributes:

Definition 3.3.1 (Family Write Attributes). A family F is writing, nonwriting single-writing, multiple-writing, iff the arc (F.start, F.guard [right arrow] F.assig, F.finish) is writing, nonwriting, single-writing, multiple-writing, respectively.

For the "guarding" attributes, we find it technically convenient to use the following definition instead.

Definition 3.3.2 (Unguarded Family, Guarded Family). A [P.sub.i]-family F is unguarded in Kripke structure M = ([S.sub.0], S, R) iff:

for all reachable states s in M such that s [up arrow] i = F.start, there exists a transition T [member of] F such that T.begin = s

A [P.sub.i]-family F is guarded in M iff F is not unguarded in M.

In other words, an unguarded family contains a transition starting in every reachable state s whose [P.sub.i]-projection s [up arrow] i is equal to the start state of the family. Hence the [P.sub.i]-arc (F.start, F.guard [right arrow] F.assig, F.finish) extracted from F can be executed in every state s such that s [up arrow] i = F.start. Hence s [satifies] {F.start} implies s [satifies] F.guard for every reachable state s. We can rewrite this as s [satifies] {F.start} [??] (F.guard [equivalent to] true). Thus F.guard can be replaced by true, and so the arc extracted from an unguarded family is also unguarded. (11) Also, if [AR.sub.i] is an unguarded arc in program P, then the [P.sub.i]-family that [AR.sub.i] generates in the global-state transition diagram of P (according to the global-state transition diagram definition (2.2.2)), is also unguarded.

Consider a guarded [P.sub.i]-family F in M. If we apply the program extraction definition (2.3) to extract a program from M, then the [P.sub.i]-arc corresponding to F will have the guard F.guard, which, by the [P.sub.i]-family definition (2.2), is [V.sub.T [member of] F] {T.begin [down arrow] i}. By the state-to-formula definition (2.1), {T.begin [down arrow] i} is a conjunction of simple terms. Thus we see that F.guard is in disjunctive normal form, with each disjunct being a conjunction of simple terms. The atomic read/write program definition (3.1.4) requires that every guard in an atomic read/write program be a disjunction of simple terms. Hence, to extract an atomic read/write program from M, we must replace F.guard by an equivalent (12) guard which is a disjunction of simple terms. If this can be done, then the [P.sub.i]-family F can be implemented by a single-reading arc. We call such a family a single-reading family:

Definition 3.3.3 (Single-Reading Family). A family F of a Kripke structure M is single-reading iff there exist subsets [F.sub.1], ..., [F.sub.n] of F such that F = [U.sub.k [member of] [1:n]] [F.sub.k], and, for each [F.sub.k], (k [member of] [1 : n]), there exists a simple term [b.sub.k] such that

(G1) for all T [element of] [F.sup.r.sub.k], begin([b.sub.k]) = true, and

(G2) for all reachable states s in M such that s [up arrow] i = F.start, if s is not the start state of some transition in [F.sub.k], then s([b.sub.k]) = false,

where [F.sup.r.sub.k] is the set of all reachable transitions in [F.sub.k].

In other words, [b.sub.k] is true in all states that are the begin state of some reachable transition in [F.sub.k], and is false in any reachable state whose [P.sub.i]-projection is the start state of F, but which is not the begin state of some transition in [F.sub.k]. Thus, including [b.sub.k] as a disjunct in the guard of the arc corresponding to F takes into account exactly the reachable transitions in [F.sub.k]. Hence, the guard [V.sub.k [member of] [1:n]] [b.sub.k] takes into account all reachable transitions in F (since F = [U.sub.k[element of][1:n]] [F.sub.k]). Furthermore, requiring that [b.sub.k] be false in every state s such that s [up arrow] i = F.start and such that s is not the start state of some transition in [F.sub.k] ensures that no "extra" transitions are generated by the extracted programs (i.e., no transitions that are not present in the reachable portion of the Kripke structure from which the program is extracted). Thus [V.sub.k [member of] [1:n]] [b.sub.k] is a suitable guard for the arc corresponding to F. Also, [V.sub.k [member of] [1:n]] [b.sub.k] is a disjunction of simple terms, as required.

We can now define atomic read/write Kripke structures. From such a structure, it is always possible to extract an atomic read/write program. Note how this definition parallels that of atomic read/write programs (Definition 3.1.4 above).

Definition 3.3.4 (Atomic Read/Write Kripke Structure). M = ([S.sub.0], S, R) is an atomic read/write Kripke structure iff M is a Kripke structure such that every family in M is either single-reading and nonwriting, or unguarded and single-writing.

3.4 Extracting Atomic Read/Write Programs from Atomic Read/Write Kripke Structures

Given an atomic read/write Kripke structure M, an atomic read/write program P can be extracted from M according to the following definition, which is a modification of the program extraction definition (2.3).

Definition 3.4.1 (Atomic Read/Write Program Extraction Definition). Let M be an atomic read/write Kripke structure. Then, the program P = [P.sub.1] [parallel] ... [parallel] [P.sub.K] extracted from M is as follows:

([s.sub.i], B [right arrow] skip, [t.sub.i]) [member of] [P.sub.i] iff

there exists a single-reading and nonwriting [P.sub.i]-family F in M such that [s.sub.i] = F.start, [t.sub.i] = F.finish, B = [V.sub.k [member of] [1:n]] [b.sub.k], and there exist

subsets [F.sub.1], ..., [F.sub.n] of F such that

[F.sub.1] , ..., [F.sub.n], [b.sub.1], ..., [b.sub.n] satisfy Definition 3.3.3

([s.sub.i], true [right arrow] A, [t.sub.i]) [member of] [P.sub.i] iff

there exists an unguarded, single-writing [P.sub.i]-family F in M such that

[s.sub.i] = F.start, [t.sub.i] = F.finish, and A = F.assig

PROPOSITION 3.4.2. If P has been extracted from an atomic read/write Kripke structure M according to Definition 3.4.1, then P is an atomic read/write program.

PROOF. By Definition 3.4.1, the only arcs in P are of the form ([s.sub.i], B [right arrow] skip, [t.sub.i]) or of the form ([s.sub.i], true [right arrow] A, [t.sub.i]). For arcs of the form ([s.sub.i], B [right arrow] skip, [t.sub.i]), B is a disjunction of simple terms, by Definition 3.4.1 and Definition 3.3.3. Hence, such arcs are single-reading and nonwriting. For arcs [AR.sub.i] of the form ([s.sub.i], true [right arrow] A, [t.sub.i]), the corresponding family F is single-writing, by Definition 3.4.1. Thus, by the family write attributes definition (3.3.1), [AR.sub.i] is single-writing (since [s.sub.i] = F.start, [t.sub.i] = F.finish, and A = F.assig). Hence [AR.sub.i] is unguarded and single-writing. Thus, every arc in P is either single-reading and nonwriting, or unguarded and single-writing. Hence, by the atomic read/write program extraction definition (3.4.1), P is an atomic read/write program. []

The next lemma establishes that the atomic read/write extraction operation is "faithful" in that the global-state transition diagram of the extracted program is the same as the reachable portion of the original Kripke structure from which the program was extracted.

LEMMA 3.4.3 (CORRECT EXTRACTION). Let [M.sup.1] = ([S.sub.0], S, [R.sup.1]) be an atomic read/write Kripke structure. Furthermore, let P = [P.sub.1] [parallel] ... [parallel] PK be an atomic read/write program extracted from [M.sup.1] using Definition 3.4.1, and let [M.sup.2] = ([S.sub.0], S, [R.sup.2]) be the global-state transition diagram of P obtained by applying Definition 2.2.2 to P. If a state s is reachable in both [M.sup.1] and [M.sup.2], then

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

for all i, A, t.

PROPOSITION 3.4.4. Let [M.sup.1] = ([S.sub.0], S, [R.sup.1]) be an atomic read/write Kripke structure. Furthermore, let P be an atomic read/write program extracted from [M.sup.1] using Definition 3.4.1, and let [M.sup.2] = ([S.sub.0], S, [R.sup.2]) be the global-state transition diagram of P obtained by applying Definition 2.2.2 to P. Let f be an arbitrary formula of CTL. Then

[M.sup.1], [S.sub.0] [satifies] f iff [M.sup.2], [S.sub.0] [satifies] f.

4. THE SYNTHESIS METHOD

Let f be a specification, expressed in CTL, for a concurrent program. Roughly speaking, we proceed as follows. We apply the CTL decision procedure of Emerson and Clarke [1982] to f. If f is satisfiable, then the decision procedure yields a model M of f. M can be viewed as the global-state transition diagram of a program P that satisfies f, and P can be extracted from M via the program extraction definition (2.3). In general, P will contain arbitrarily large grain test-and-set operations. We decompose these operations into single atomic read and single atomic write operations. The decomposition is straightforward and syntactic in nature; a test-and-set operation is decomposed into a test operation followed by a (multiple-)write operation, and a multiple-write operation is decomposed into a set of sequences of single-write operations which express all the possible serializations of the multiple-write operation. This decomposition may, in general, introduce new behaviors that violate the specification. We deal with this by generating the global-state transition diagram of the decomposed program, and then deleting all the portions of this diagram that are inconsistent with the specification. If some initial state is not deleted, then, from the resulting structure, an atomic read/write program that satisfies the specification can be extracted.

Our method will be presented as a sequence of phases, with each phase (except Phase 1) taking as input the output of the previous phase:

Phase 1 Extract a correct high-atomicity program from M, a finite-state model of the CTL problem specification.

Phase 2 Decompose the high-atomicity program into an atomic read/write program by syntactically decomposing each arc of each process.

Phase 3 Generate the global-state transition diagram of the atomic read/write program.

Phase 4 Delete portions of the global-state transition diagram that violate the specification.

Phase 5 From the resulting global-state transition diagram, extract an atomic read/write program that satisfies the specification.

In Phase 1, M could be given directly, as a "specification automaton," or could be produced from the CTL specification by the synthesis method of Emerson and Clarke [1982], whose application could then be considered to be "Phase 0." For technical reasons, we assume that M is in reachable form. Since only the reachable portion of a Kripke structure affects the behavior of an extracted program, this assumption does not restrict our synthesis method in any way. Furthermore, in practice we would wish to remove the unreachable portion of a Kripke structure simply as a matter of efficiency. (13) Note also that the externally visible location counter (which encodes the atomic propositions) is not introduced until Phase 2; Phase 1 deals directly with the atomic propositions.

4.1 Phase 1: Synthesize a Correct High-Atomicity Program

The objective of this phase is to synthesize an initial program that satisfies the specification f, but is not necessarily in atomic read/write form.

4.1.1 Step 1.1: Derive the Initial Kripke Structure. Our method accomodates a variety of problem specification techniques. If the problem specification is given as a CTL formula f, then we can apply the CTL decision procedure of Emerson and Clarke [1982] to f. If f is unsatisfiable, then no program can satisfy f. Otherwise, f is satisfiable, and the decision procedure yields a Kripke structure M = ([S.sub.0], S, R) such that M, [S.sub.0] [satifies] f, i.e., M is a model of f.

Alternatively, we can specify M directly, i.e., we view M as a state-machine whose executions constitute a set of "acceptable" executions. Examples of this technique are Lynch and Tuttle [1987], Lynch and Vaandrager [1995]. Even if M is given directly, our method still requires a CTL specification f which expresses the acceptable behaviors. This is because the decomposition performed in Phase 2 may introduce new and undesirable behaviors, which have to be pruned out. The only way to determine which behaviors are undesirable is to have a specification against which to judge the new behaviors introduced by Phase 2. We have chosen to use a restricted subset of CTL for the purpose of writing these specifications. The main advantage is that the modifications required to eliminate the undesirable behaviors (and thereby restore the satisfaction of the specification) are reasonably straightforward (cf. the deletion rules in Section 4.4).

If M is given directly, then the accompanying CTL specification is usually significantly shorter than if the specification were given only as a CTL formula. This is because many of the conjuncts of a CTL specification are "frame specifications" which specify the initial state (e.g., clause 1 in the CTL specification of two-process mutual exclusion given in Section 2.4), the local structure of each process (clauses 2, 3, 4, and 5), the interleaving model (clause 7), and deadlock-freedom (clause 9). When M is given, such frame specifications can be extracted mechanically from M, as shown in Figure 4. They are then conjoined to the CTL specification accompanying M, and used as the specification for the purposes of the remaining steps in our synthesis method. (Except that the interleaving model clause is not needed, since it is implicitly satisfied by our operational semantics. The need for this clause arises in the Emerson and Clarke [1982] synthesis method.)
Fig. 4. Extracting the CTL frame specification from a finite-state
machine specification.

Given a finite-state machine speficiation M, extract the corresponding
CTL frame specification as the conjunction of all the formulae
specified by the following rules.

Initial state: [V.sub.s] is an initial state{s}

Local AY-structure of each process: for all [P.sub.i]: AG({[s.sub.i]}
[??] [AY.sub.i][V.sub.l]{t.sup.l.sub.i]}) where [t.sub.l.sub.i] ranges
over all the [P.sub.i]-states such that some arc of [P.sub.i] goes
from [s.sub.i] to [t.sup.l.sub.i].

Local EX-structure of each process: for all [P.sub.i]: AG({[s.sub.i]}
[??] [EX.sub.i]{[t.sub.i]}) if, in M, every global state s with s
[up arrow] i = [s.sub.i] has some successor state t reached by a
[P.sub.i]-transition such that t [up arrow] i = [t.sub.i].

The interleaving model: for all [P.sub.i], [P.sub.j] ,i [not equal to]
j and [Q.sub.i] [member of] [AP.sub.i]: AG([Q.sub.i] [??] [AY.sub.j]
[Q.sub.i])

Deadlock-freedom: AGEXtrue


For example, looking at the CTL specification of two-process mutual exclusion given in Section 2.4, we see that clauses 8 and 6 express the crucial safety and liveness properties required of a solution to mutual exclusion. Thus, an alternative specification of mutual exclusion would be the Kripke structure of Figure 2, together with the (much shorter) CTL formula AG([logical not] ([C.sub.1] [conjunction] [C.sub.2])) [and] AG([T.sub.1] [??] [AFC.sub.1]) [conjunction] AC([T.sub.2] [??] [AFC.sub.2]).

We note, that when M and f are both given, then we do not require M, [s.sup.0] [satifies] f for every initial state [s.sup.0] of M. In other words, the given finite-state machine is not required to be "correct." Thus, our method provides both debugging and refinement, in this case.

4.1.2 Step 1.2: Replicate Multiple Assignments. First, we transform M = ([S.sub.0], S, R) into an "equivalent" Kripke structure M' = ([S'.sub.0], S, R') such that every multiple assignment [//.sub.m [member of] [1:n]] [x.sup.m] := [c.sup.m] in M is replicated along all "compatible" transitions. This has the desirable effect of weakening the guard of the assignment [//.sub.m [member of] [1:n]] [x.sup.m] := [c.sup.m] in the program extracted from M'.

Let [//.sub.m [member of] [1:n]] [x.sup.m] := [c.sup.m] be a multiple assignment that labels some [P.sub.i]-transition [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] in M. We replicate this assignment along every [P.sub.i]-transition [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] in M such that u [up arrow] i = s [up arrow] i, v [up arrow] i = t [up arrow] i, (i.e., every [P.sub.i]-transition which takes [P.sub.i] from the same (local) start state to the same (local) finish state) and A does not assign to any of [x.sup.1], ..., [x.sup.n]. After this replication is performed (for all multiple assignments in M), it is possible that some states in M end up with two or more different values for the same shared variable, due to the extra assignments introduced. We therefore apply the following "propagation rules" (which "propagate" the resulting values of all shared variables) repeatedly to M, until none of the rules produces any change:

add-prop If a transition into state s is labeled with x := c then add the binding < x, c > to s [up arrow] SH. (14)

split-state If state s contains bindings < x, [c.sup.1] >, ..., < x, [c.sup.k] > (k > 1) then replace s by k propositionally equivalent (15) states [s.sup.1], ..., [s.sup.k], where [s.sup.l] contains < x, [c.sup.l> and all bindings of s not involving x (l [member of] [1 : k]). Each [s.sup.l] has the same outgoing transitions as s, but has as incoming transitions only the incoming transitions of s that are consistent (16) with x = [c.sup.l].

propagate-value If state s contains < x, c > and there exists a transition from s to s' not labeled with an assignment to x, then add < x, c > to s'.

The function of the above three rules is to resolve any inconsistencies that arise due to the replication of multiple assignments by creating new global states as needed. The three rules above cannot introduce any new cycles, nor any states that are not propositionally equivalent to a state already occurring in M. Also, termination is guaranteed since the number of possible states and/or transitions is finite; hence, eventually no new states and/or transitions can be added. Finally, we let the set of initial states of M', namely [S'.sub.0], be

{s | s is a state of M' and s is propositionally equivalent to some state in [S.sub.0]}.

PROPOSITION 4.1.2.1. Let f be an arbitrary formula of CTL. Then

M, [S.sub.0] [satifies] f iff M', [S'.sub.0] [satifies] f.

PROOF. It is straightforward to establish a bisimulation [Clarke et al. 1986] between M and M': every state in M is bisimilar to all states M' that are propositionally equivalent to it. Since the only rule that adds new states is split-state, and since this rule preserves all outgoing transitions, i.e., all successor states, it follows (by a simple induction) that propositionally equivalent states are indeed bisimilar. Theorem 2 of Clarke et al. [1986] is as follows:

Let [M.sup.1] and [M.sup.2] be two structures that correspond. Then for all formulae f of CTL*, [M.sup.1], [s.sup.1.sub.0] [satifies] f iff [M.sup.2], [s.sup.2.sub.0] [satifies] f.

Here the term "correspond" means "are bisimilar." Although this theorem is given for structures [M.sub.1], [M.sub.2] with single initial states [s.sub.1.sub.0], [s.sup.2.sub.0] respectively, it is easily seen to generalize to structures with a set of initial states. Furthermore, the logic CTL* [Emerson 1990] subsumes CTL. Thus, applying the theorem to M, M', we conclude: M, [S.sub.o] [satifies] f iff M', [S'.sub.0] [satifies] f for any formula f of CTL. []

4.1.3 Step 1.3: Extract a Correct High-Atomicity Program. Next, we extract a correct high-atomicity program P = [P.sub.1] [parallel] ... [parallel] from M' using the program extraction definition (2.3). We mention our convention, which we use in all figures of Kripke structures (synchronization skeletons), of showing in a global (local) state only the atomic propositions that are true in that global (local) state. The atomic propositions not shown can be taken to be false in the global (local) state. Note also, that in all figures of Kripke structures, we show only the reachable portions of the actual structures.

4.1.4 Step 1.4: Simplify the Guards. The program extraction definition (2.3) produces guards that are in disjunctive normal form, where each disjunct contributes exactly one transition. Each guard, in principle, may read the entire global state, i.e., the atomic propositions of all other processes, and the values of all shared variables. Often, it is not necessary to read all the components of the global state, and the guards can be "simplified" considerably.

Consider an arbitrary arc ([s.sub.i], B [right arrow] A, [t.sub.i]) of [P.sub.i]. The guard B is tested only in global states whose [P.sub.i]-component is [s.sub.i]. Hence, B can be replaced by any B' that has the same value as B in all such global states, and possibly differs from B in other global states. Hence, any B' such that

(GS) for all s [member of] S : s [up arrow] i = [s.sub.i] implies s [satifies] (B [equivalent to] B')

can be used as a guard instead of B, i.e., the arc ([s.sub.i], B [right arrow] A, [t.sub.i]) is replaced by ([s.sub.i], B' [right arrow] A, [t.sub.i]).

Two special cases of (GS) that are useful in practice are as follows:

Guard elimination: B' = true. If we establish for all s [member of] S : s [up arrow] i = [s.sub.i] implies s [satifies] B

then B can be replaced by true, i.e., the arc is enabled whenever "local control" is at its start state.

Conjunct elimination: B = B" [disjunction] ([b.sub.1][conjunction] ... [conjunction][b.sub.n]), and B' = B"[disjunction] ([b.sub.i][conjunction] ... [conjunction][b.sub.n-1]). If we establish

for all s [member of] S : s [up arrow] i = [s.sub.i] implies s [satifies] [([b.sub.1][conjunction] ... [conjunction][b.sub.n-1]) [??] [b.sub.n]]

then B can be replaced by B', since we would have:

for all s [member of] S : s [up arrow] i = [s.sub.i] implies s [satifies] [([b.sub.1][conjunction] ... [conjunction][b.sub.n-1]) [equivalent to] ([b.sub.1][conjunction] ... [conjunction][b.sub.n])] and so

for all s [member of] S : s [up arrow] i = [s.sub.i] implies s [satifies] [B"[disjunction]([b.sub.1][conjunction] ... [conjunction][b.sub.n-1]) [equivalent to] B"[disjunction]([b.sub.1][conjunction] ... [conjunction][b.sub.n])].

Since the program extraction definition (2.3), produces guards in disjunctive normal form, this simplification method should be quite useful.

4.2 Phase 2: Decompose the Initial Program

4.2.1 Step 2.1: Introduce the Externally Visible Location Counters. We now introduce the externally visible location counter [L.sub.i], and replace all references to the atomic propositions in [AP.sub.i] by references to [L.sub.i]:

--Every occurrence of an atomic proposition [Q.sub.i] [member of] [AP.sub.i] in some guard B (occurring in the skeleton for some process [P.sub.j], j [not equal to] i) is replaced by "[Q.sub.i] [member of] [L.sub.i]."

--Every arc ([s.sub.i], B [right arrow] A, [t.sub.i]) of [P.sub.i], such that L[[s.sub.i]] [not equal to] L[[t.sub.i]], is replaced by the arc ([s.sub.i], B [right arrow] A//[L.sub.i] := L[[t.sub.i]],[t.sub.i]).

The first transformation replaces a read of an atomic proposition in [AP.sub.i] by a read of [L.sub.i]. The second transformation ensures that [L.sub.i] implements the atomic propositions in [AP.sub.i] correctly; in other words, it ensures that LOC (Section 2.2) holds for every i-state in [P.sub.i]. We extend the definition of global state to provide for a value assigned to [L.sub.i] by a global state s: s([L.sub.i]) = s [up arrow] i([L.sub.i]). Finally, we mention that the state-to-formula definition (2.1) should be modified (to take into account the introduction of the [L.sub.i]) as follows: every conjunct of the form [Q.sub.i], ([logical not][Q.sub.i]) is replaced by [Q.sub.i] [member of] [L.sub.i] ([Q.sub.i] [not member of] [L.sub.i]) respectively.

Since L[[t.sub.i]] is constant for a given local state [t.sub.i], the assignment [L.sub.i] := L[[t.sub.i]] can be implemented by a single atomic write operation. Thus, the assignment operation A of an arc ([s.sub.i], B [right arrow] A, [t.sub.i]) has the form [//.sub.m [member of] [1:n]][A.sup.m], (n [greater than or equal to] 0), where each [A.sup.m] has either the form x := c (x [member of] SH, c [member of] [D.sub.x]), or the form [L.sub.i] := L[[t.sub.i]], with at most one [A.sup.m] having the latter form. If L[[s.sub.i]] = L[[t.sub.i]], then no [A.sup.m] has the form [L.sub.i] := L[[t.sub.i]], and if L[[s.sub.i]] [not equal to] L[[t.sub.i]], then exactly one [A.sup.m] has this form.

4.2.2 Step 2.2: Decompose the Test-and-Set Arcs. Our next step is to decompose every test-and-set arc in P into a guarded and nonwriting arc (for the "test"), followed by an unguarded and writing arc (for the "set"):

--For every test-and-set arc AR = ([s.sub.i], B [right arrow] A, [t.sub.i]) replace AR by AR' and AR", where AR' = ([s.sub.i], B [right arrow] skip, [u.sub.i]) AR" = ([u.sub.i], true [right arrow] A, [t.sub.i])

where [u.sub.i] is a "new" i-state (i.e., it does not already occur in [P.sub.i]), and L[[u.sub.i]] is set to L[[s.sub.i]].

4.2.3 Step 2.3: Decompose the Multiple-Writing Arcs and Number the Local States. Finally, we replace every unguarded and multiple-writing arc by a set of sequences of unguarded and single-writing arcs, where each sequence represents one order of serialization of the write operations of the original multiple-writing arc:

--For every multiple-writing arc AR = ([u.sub.i], true [right arrow] [//.sub.m [member of] [1:n][A.sup.m]], [t.sub.i]) remove AR from P; for every permutation [m.sub.1], ..., [m.sub.n] of 1, ..., n, add [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII], ..., [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] to P, where [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] for k [member of] [2 : n - 1] [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

where the i-states [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII], ..., [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] do not previously occur in P (for every permutation), i.e., we use "new" local states for each permutation.

Also, the local atomic proposition valuations of the new local states are given as follows:

--If [//.sub.m [member of] [1:n]][A.sup.m] does not assign to [L.sub.i], (and so no [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] has the form [L.sub.i] := L[[t.sub.i]]), then set [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] to L[[s.sub.i]] for all k in [1 : n - 1].

--If [//.sub.m [member of] [1:n]][A.sup.m] assigns to [L.sub.i], then exactly one [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII], l [member of] [1 : n] has the form [L.sub.i] := L[[t.sub.i]]. In this case:

set [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] to L[[s.sub.i]] for all k in [1 : l - 1]

set [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] to L[[t.sub.i]] for all k in [l : n - 1]

Call the resulting program P' = [P'.sub.1] [parallel] ... [parallel] [P'.sub.K]. Looking at Figure 13, we see that it contains propositionally equivalent but distinct local states. We now assign numbers to local states (see Section 3.2) so that all propositionally equivalent but distinct local states in P' are distinguished from each other by their numbers (i.e., so that (NUM)--see Section 3.2--holds).

Let P" = [P".sub.1] [parallel] ... [parallel] [P".sub.K] be the program that results from the local state numbering. We can now state the following proposition. To facilitate its proof, we shall make the following assumption:

Technical Assumption: P contains no arcs that are both unguarded and nonwriting.

If P does contain such arcs, we can always convert them to single-writing arcs by adding a new atomic proposition which is "written to" by such arcs, but is never "read" by any arc, and so does not change P's behavior.

PROPOSITION 4.2.3.1. Every arc in the skeletons of P" is either guarded and nonwriting, or unguarded and single-writing.

PROOF. By construction of Phase 2, P" contains no test-and-set arcs. Hence by the syntactic arc attributes definition (3.1.2), every arc in P" is nonwriting or unguarded. By this and the technical assumption (given immediately above), every arc in P" is guarded and nonwriting or unguarded and writing. Finally, by construction of Phase 2, P" contains no multiple-writing arcs. Hence every arc in P" is guarded and nonwriting or unguarded and single-writing. []

4.3 Phase 3: Generate the Global-State Transition Diagram

In Phase 3, we generate the global-state transition diagram M" = ([S'.sub.0], S, R") of P" by applying the global-state transition diagram definition (2.2.2) to P". (17)

Our use of local-state numbers makes it clear which local states a global state projects onto. For example, the state [[T.sup.2.sub.1] 2 [N.sup.1.sub.2]] in Figure 15 has a [P.sub.1]-projection of [[T.sup.2.sub.1]], i.e., the 1-state indicated by [[T.sup.2.sub.1] in Figure 14. Since there are two other propositionally equivalent [P.sub.1]-states in Figure 14, namely those labeled with [T.sup.1.sub.1], [T.sup.3.sub.1] respectively, it would be impossible to distinguish these [P.sub.1]-states from the [P.sub.1]-state labeled with [T.sup.2.sub.1] were it not for the use of local-state numbers.

4.4 Phase 4: Delete Portions of the Global-State Transition Diagram that Violate the Specification

The global-state transition diagram generated in Phase 3 will not, in general, satisfy the CTL specification. This is because the syntactic decomposition of the skeleton arcs performed in Phase 2 introduces the possibility of new interleavings, leading to computation paths that generate previously unreachable states. For example, suppose that the arcs A[R.sub.i], A[R.sub.j] in processes [P.sub.i], [P.sub.j] of P = [P.sub.1] [parallel] ... [parallel] [P.sub.K] are decomposed into arcs A[R.sup.1.sub.i], A[R.sup.2.sub.i] and A[R.sup.1.sub.j], A[R.sup.2.sub.j] respectively, in the processes [P".sub.i], [P".sub.j] of the decomposed program P" = [P".sub.1] [parallel] ... [parallel] [P".sub.K] produced by Phase 2. In the execution of P, either A[R.sub.i] is executed before A[R.sub.j] or vice versa. In the execution of P", it is possible for the execution of A[R.sup.1.sub.i], A[R.sup.2.sub.i] and A[R.sup.1.sub.j], A[R.sup.2.sub.j] to be interleaved, e.g., A[R.sup.1.sub.i]; A[R.sup.1.sub.j]; A[R.sup.2.sub.i], A[R.sup.2.sub.j]. This represents a new behavior, not possible in program P. Such new behaviors can lead to global states (or cycles of global states) that were previously unreachable. These new states/cycles could violate the specification. For example, in Figure 15, the dashed path results from such a new behavior, and leads to the state [[C.sup.1.sub.1] 2 [C.sup.1.sub.2]], which violates the conjunct AG([logical not]([C.sub.1] [conjunction] [C.sub.2])) of the mutual exclusion specification.

Our solution to this problem is to delete all portions of the global-state transition diagram that violate the specification. Provided that not all initial states are deleted as a result, the remaining structure will then satisfy the specification, and a correct atomic read/write program could be extracted from it. We proceed as follows.

4.4.1 Step 4.1: Label the Reachable States. First, we label every reachable state of M" with a set of CTL formulae. The label of each state (notated as label(s)) contains exactly the CTL formulae that must be satisfied by that state in order that every initial state of M" satisfy the specification. The labeling procedure is given in Figure 5.

Fig. 5. The labeling rules.

For each conjunct f of the specification, except those of the form AG([p.sub.i] [??] A[Y.sub.i][q.sub.i]), label the states of M" according to the following labeling rules, where p, q, r, h [member of] LO(AP, [logical not], [conjunction]), and [p.sub.i], [q.sub.i] [member of] LO(A[P.sub.i], [logical not], [conjunction]).

--If f = h, then label every initial state in M" (i.e., every state in [S'.sub.0]) with h.

--If f = AGh, then label every reachable state in M" with h.

--If f = AG(p [??] A[q [union] r]) then label every reachable state s in M" such that s [satisfies] p with A[q [union] r].

--If f = AG([p.sub.i] [??] E[X.sub.i][q.sub.i]) then label every reachable state s in M" such that s [satisfies] [p.sub.i] with E[X.sub.i] ([p.sub.i] [disjunction] [q.sub.i]).

4.4.2 Step 4.2: Prune the Structure So that the Labels Are Satisfied. Next, we check that every state of M" satisfies all the formulae in its label. If some state of M" does not satisfy a formula in its label, then M" does not satisfy the specification and must be modified. We modify M" by deleting initial states and transitions. Now deleting a single transition T[R.sub.i] (of some process [P".sub.i] of P") may cause the arc A[R.sub.i] corresponding to the family containing T[R.sub.i] to become guarded. If A[R.sub.i] was previously single-writing, then A[R.sub.i] now becomes test-and-set. We avoid this possibility by deleting all transitions of the family containing T[R.sub.i], thereby deleting A[R.sub.i] entirely. However, this may leave [P".sub.i] incapable of infinite behavior, e.g., if [P".sub.i] was previously a single "cycle." We say that an arc A[R.sub.i] of [P".sub.i] is deletable iff its deletion leaves at least one cycle in [P".sub.i], i.e., leaves [P".sub.i] capable of infinite behavior. Otherwise we say that A[R.sub.i] is nondeletable. We only delete transitions in M" that correspond to deletable arcs. A transition T[R.sub.i] is deleted by invoking the procedure delete (T[R.sub.i]), shown in Figure 6.
Fig. 6. The delete transition procedure.

procedure delete(T[R.sub.i])

Let [F.sub.i] be the family in M" containing T[R.sub.i], and let
A[R.sub.i] be the skeleton arc corresponding to [F.sub.i].
if [F.sub.i] is guarded and nonwriting then
                remove T[R.sub.i] from M";
                if [F.sub.i] is now empty, then remove
                A[R.sub.i] from [P".sub.i]
else ([F.sub.i] is unguarded and single-writing)
                remove all transitions in [F.sub.i] from M";
                remove A[R.sub.i] from [P".sub.i]
endif;
recompute the "deletable" attribute for all arcs of [P".sub.i]


The actual deletions to be carried out are given by a set of deletion rules, shown in Figure 7. The deletion rules are applied as long as possible. Since M" is finite, and each application of a deletion rule results in the deletion of at least one state or one transition in M", we eventually terminate, i.e., reach a situation in which none of the deletion rules are applicable. Upon termination, let [S"'.sub.0], R"' be the set of undeleted initial states, undeleted and reachable (from [S"'.sub.0]) transitions, respectively. If [S"'.sub.0] is empty, then all the initial states have been deleted, and we are therefore unable to extract a program from M" that satisfies the problem specification. In this case, our synthesis method terminates with failure. This possibility of termination with failure means that our synthesis method is not complete, i.e., it may not always produce an atomic read/write program satisfying a given specification, even if such a program does in fact exist. The method is sound however, as we subsequently establish. If [S"'.sub.0] is nonempty, let M"' be the structure ([S"'.sub.0], S, R"'). We show that M"' satisfies the CTL specification.

Fig. 7. The deletion rules.

Prop-rule h [member of] label(s) and s [not satisfies] h.

If s [member of] [S'.sub.0], then delete s. Otherwise, make s unreachable in M", i.e., find one deletable transition T[R.sub.i] from every initialized path ending in s, and remove T[R.sub.i] from M" by invoking delete(T[R.sub.i]) (an initialized path is a path starting in an initial state).

A[union]-rule A[q [union] r] [member of] label(s) and s [not satisfies] A[q [union] r].

Find one deletable transition T[R.sub.i] from every fullpath [pi] starting in s such that [pi] [not satisfies] [q [union] r], and remove T[R.sub.i] from M" by invoking delete (T[R.sub.i]).

E[X.sub.i]-rule E[X.sub.i]([p.sub.i] [disjunction] [q.sub.i]) [member of] label(s) and s [not satisfies] E[X.sub.i]([p.sub.i] [disjunction] [q.sub.i]). If s [member of] [S'.sub.0], then delete s. Otherwise, make s unreachable in M", as in the Prop-rule.

EX-rule s [not satisfies] EXtrue, i.e., s has no successors. If s [member of] [S'.sub.0], then delete s. Otherwise, make s unreachable in M", as in the Prop-rule.

Arc-rule ([s.sub.i], B [right arrow] A, [t.sub.i]) is an arc in [P".sub.i] such that either (1) [P".sub.i] contains no arc with start state [t.sub.i], or (2) [P".sub.i] contains no arc with finish state [s.sub.i], and [s.sub.i] [not member of] [S'.sub.0] [up arrow] [i.sup.18] (i.e., [s.sub.i] is not an initial local state).

Remove ([s.sub.i], B [right arrow] A, [t.sub.i]) from [P".sub.i], and its corresponding family from M".

The name and activation condition (for a particular reachable state s) of each rule is given first, with the action required by the rule given on succeeding lines. For all the above rules, whenever a state s in [S'.sub.0] is deleted, all transitions in R" which involve s (as either a begin or end state) are also deleted. If any of these transitions are undeletable, then the synthesis method terminates with failure.

PROPOSITION 4.4.2.1 (SOUNDNESS). If [S"'.sub.0] [not equal to] 0, and f is a conjunct of the specification, then

M"', S"' [satisfies] [f.sup.*]

where [f.sup.*] = f if f has one of the forms h, AGh, AG(p [??] A[q [union] r]), and [f.sup.*] = AG([p.sub.i] [??] E[X.sub.i]([p.sub.i] [disjunction] [q.sub.i])), AG([p.sub.i] [??] A[Y.sub.i]([p.sub.i] [disjunction] [q.sub.i])) if f = AG([p.sub.i] [??] E[X.sub.i][q.sub.i]), AG([p.sub.i] [??] A[Y.sub.i][q.sub.i]) respectively, and where p, q, r, h [member of] LO(AP, [logical not], [conjunction]), [p.sub.i], [q.sub.i] [member of] LO([AP.sub.i], [logical not], [conjunction]).

PROPOSITION 4.4.2.2. Every family in M"' is either guarded and nonwriting or unguarded and single-writing.

PROOF. By Proposition 4.2.3.1, every arc in the skeletons of P" is either guarded and nonwriting, or unguarded and single-writing. Now M" is generated by applying the global-state transition diagram definition (2.2.2) to P". From the global-state transition diagram definition (2.2.2) and the unguarded family definition (3.3.2), we see that an unguarded arc generates an unguarded family. From the global-state transition diagram definition (2.2.2), and the family write attributes definition (3.3.1), a nonwriting (single-writing) arc generates a nonwriting (single-writing) family, respectively.

Hence every family in M" is either guarded and nonwriting or unguarded and single-writing. By construction of Phase 4, every unguarded family in M" either survives intact, i.e., none of its transitions are deleted, and hence it is unguarded (and single-writing) in M"', or is deleted entirely. Thus the only guarded families in M"' are (subsets of) those that were guarded in M". Thus, by the family write attributes definition (3.3.1) these families are nonwriting in M"', since they are nonwriting in M". Since every family in M"' corresponds to a family in M", the proposition follows. []

4.5 Phase 5: Extract a Correct Atomic Read/Write Program

4.5.1 Step 5.1: Ensure Atomic Read/Write Form. The Kripke structure produced by Phase 4 is not, in general, guaranteed to be in atomic read/write form. What is missing is that the guarded and nonwriting families must be single-reading and nonwriting. Boolean function CHECK-STRUCTURE(M) given in Figure 8 tests all guarded and nonwriting families in a Kripke structure M, and returns true iff they are all single-reading as well. We invoke CHECK-STRUCTURE(M"'). If this returns true, then, by Proposition 4.4.2.2, we can conclude that every family in M"' is either single-reading and nonwriting, or unguarded and single-writing, i.e., that M"' is an atomic read/write Kripke structure. Given that M"' is in atomic read/write form, the atomic read/write program extraction definition (3.4.1) can be applied to extract the final atomic read/write program. If, however, M"' is not in atomic read/write form, then there are one or more guarded and nonwriting families that do not satisfy (at least one of) the conditions (G1), (G2) of the single-reading family definition (3.3.3). For each such family, we attempt to make (G1) and (G2) true by deleting reachable states that violate (G1) or (G2) (or both). Since such deletions may, in general, cause violation of the specification, we must repeat Phase 4 after one or more of these deletions are performed.
Fig. 8. Function CHECK-STRUCTURE(M) for testing the atomic read/write
form of a Kripke Structure M.

Boolean Function CHECK-STRUCTURE(M)

/* input: Kripke structure M such that every family in M is guarded
          and nonwriting or unguarded and single-writing
   output: true -- if M is an atomic read/write Kripke structure, i.e.,
                   every guarded and nonwriting family in M is
                   single-reading
           false -- otherwise
*/
for each guarded and nonwriting family F of M do
   if [logical not] CHECK-FAMILY(M, F) then return(false) endif
   /* If some guarded and nonwriting family F is not single-reading,
      then M is not in atomic read/write form */
endfor;
return(true)

Boolean Function CHECK-FAMILY(M, F)

/* input: Kripke structure M and family F of M
   output: true -- if F is single-reading (in this case, F.srguard
                   gives a suitable guard for the corresponding
                   extracted arc)
           false -- otherwise
*/
simple := {"[Q.sub.i] [member of] [L.sub.i]", "[Q.sub.i]
 [not member of] [L.sub.i]" | [Q.sub.i] [member of] A[P.sub.i],
 i [member of] [1: K]} [union] {"x = c" | x [member of] SH
 [conjunction] c [member of] [D.sub.x]};
/* simple contains all possible simple terms */
ok := 0;
for each b [member of] simple do
   if OK(M, F, b) then ok := ok [union] {b} endif
   /* Simple terms that generate only transitions in F are added to ok.
      This ensures that condition G2 of Definition 3.3.3 is satisfied.
       */
endfor;
if COV(F, ok) then
    F.srguard := "[[??].sub.b [member of] ok] b";
    return(true)
    /* If all the simple terms in ok collectively generate all the
    transitions in F, then declare F to be single-reading. This
    ensures that condition G1 of Definition 3.3.3 is satisfied. */
else
    return(false)
endif

where the predicates OK(M, F, b), COV(F, ok) are as follows:

OK(M, F, b) [equivalent to] [for all] reachable states s of M (s(b)
 = true [??] [there exists] T [member of] (T.begin= s))
         /* b is true only in states from which there is an outgoing
          transition of F */

COV(F, ok) [equivalent to] [for all] T [member of] F ([there exists]
 b [member of] ok (T.begin(b) = true))
        /* The simple terms in ok collectively generate all the
         transitions of F */


CHECK-STRUCTURE(M) works by invoking CHECK-FAMILY(M, F) for each guarded and nonwriting family F in M. CHECK-FAMILY(M, F) returns true if and only if F is single-reading, and it works as follows. Recall that a simple term is a formula of the form [Q.sub.i] [member of] [L.sub.i] or x = c. Because a simple term refers to only one variable (either [L.sub.i] or x), its value can be checked with a single atomic read operation. Recall also that the truth of a disjunction of simple terms can be verified by a single atomic read operation, namely the read of the variable referenced by a simple term disjunct that happens to be true. CHECK-FAMILY(M, F) now attempts to satisfy Definition 3.3.3 by finding a suitable "covering" [F.sub.1], ..., [F.sub.n] of F (i.e., subsets [F.sub.1], ..., [F.sub.n] of F such that F = [[union].sub.k [member of] [1:n]] [F.sub.k]) and simple terms [b.sub.1], ..., [b.sub.n] such that the transitions in each [F.sub.k] can be "generated" by including [b.sub.k] as a disjunct of the guard of F. CHECK-FAMILY(M, F) starts with the set of all possible simple terms (this is of size O([absolute value of M])). If a simple term generates only transitions in F then it is added to the set ok (see the definition of OK(b) in Figure 8). If, after all simple terms have been examined, the disjunction of the terms in ok (call them [b.sub.1], ..., [b.sub.n]) generates all the transitions in F (see the definition of COV(F, ok) in Figure 8) then [b.sub.1], ..., [b.sub.k], together with each [F.sub.k] generated by [b.sub.k], satisfy Definition 3.3.3. In this case, CHECK-FAMILY(M, F) returns true. Otherwise, it returns false.

4.5.2 Step 5.2: Extract the Atomic Read/Write Program. Once M"' is in atomic read/write form, we apply the atomic read/write program extraction definition (3.4.1) to extract the final atomic read/write program P"' = [P"'.sub.1] [parallel] ... [parallel] [P"'.sub.K].

We now establish the soundness of the synthesis method.

PROPOSITION 4.5.2.1. Let [M.sup.iv] = ([S"'.sub.0], S, [R.sup.iv]) result from applying the global-state transition diagram definition (2.2.2) to P"'. If [S"'.sub.0] [not equal to] 0, and f is a conjunct of the specification, then

[M.sup.iv], [S"'.sub.0] [satisfies] [f.sup.*]

where [f.sup.*] = f if f has one of the forms h, AGh, AG(p [??] A[q [union] r]), and [f.sup.*] = AG([p.sub.i] [??] E[X.sub.i]([p.sub.i] [disjunction] [q.sub.i])), AG([p.sub.i] [??] A[Y.sub.i]([p.sub.i] [disjunction] [q.sub.i])) if f = AG([p.sub.i] [??] E[X.sub.i][q.sub.i]), AG([p.sub.i] [??] A[Y.sub.i][q.sub.i]) respectively, and where p, q, r, h [member of] LO(AP, [logical not], [conjunction]), [p.sub.i], [q.sub.i] [member of] LO(A[P.sub.i], [logical not], [conjunction]).

PROOF. Assume that [S"'.sub.0] [not equal to] 0 and that f is a conjunct of the specification. By Proposition 4.4.2.1, we have M"', [S"'.sub.0] [satisfies] [f.sup.*]. Hence, by Proposition 3.4.4, we conclude [M.sup.iv], [S"'.sub.0] [satisfies] [f.sup.*]. []

THEOREM 4.5.2.2 (SOUNDNESS FOR SYNCHRONIZATION SKELETON MODEL).

If [S"'.sub.0] [not equal to] 0 and f is a conjunct of the specification, then P"' is an atomic read/write program that satisfies [f.sup.*], where [f.sup.*] = f if f has one of the forms h, AGh, AG(p [??] A[q [union] r]), and [f.sup.*] = AG([p.sub.i] [??] E[X.sub.i]([p.sub.i] [disjunction] [q.sub.i])), AG([p.sub.i] [??] A[Y.sub.i]([p.sub.i] [disjunction] [q.sub.i])) if f = AG([p.sub.i] [??] E[X.sub.i][q.sub.i]), AG([p.sub.i] [??] A[Y.sub.i][q.sub.i]) respectively, and where p, q, r, h [member of] LO(AP, [logical not], [conjunction]), [p.sub.i], [q.sub.i] [member of] LO(A[P.sub.i], [logical not], [conjunction]).

PROOf. Assume [S".sub.0] [not equal to] 0. By construction of Phase 5, M"' is an atomic read/write Kripke structure. Since P"' results from applying the atomic read/write program extraction definition (3.4.1) to M"' (by construction of Phase 5), we conclude by Proposition 3.4.2 that P"' is an atomic read/write program.

Finally, since [M.sup.iv] is the global-state transition diagram of P"', we conclude from Proposition 4.5.2.1 and the definition of correctness property (see Section 2.5) that P"' satisfies [f.sup.*]. []

4.6 Summary of the Method

To give an overview of our method, we summarize the steps as follows. For some steps, we indicate the Kripke structure or program that is produced (or modified) by that step.

--Phase 1: Synthesize a Correct High-Atomicity Program

Step 1.1: Derive (or Specify) the Initial Kripke Structure M

Step 1.2: Replicate Multiple Assignments (M')

Step 1.3: Extract a Correct High-Atomicity Program (P)

Step 1.4: Simplify the Guards

--Phase 2: Decompose the High-Atomicity Program

Step 2.1: Introduce the Externally Visible Location Counters

Step 2.2: Decompose the Test-and-Set Arcs

Step 2.3: Decompose the Multiple-Writing Arcs (P') and Number the Local States (P")

--Phase 3: Generate the Global-State Transition Diagram (M")

--Phase 4: Delete Portions of the Global-State Transition Diagram that Violate the Specification

Step 4.1: Label the Reachable States

Step 4.2: Prune Structure So That Labels Are Satisfied (M"')

--Phase 5: Extract a Correct Atomic Read/Write Program

Step 5.1: Ensure Atomic Read/Write Form (M"')

Step 5.2: Extract the Atomic Read/Write Program (P"')

5. EXTENDED EXAMPLE: TWO-PROCESS MUTUAL EXCLUSION

We now present a detailed example of the use of our method to synthesize an atomic read/write solution to the two-process mutual exclusion problem. We show the working of each phase of our method, along with the intermediate results.

We note that whenever the atomic propositions in A[P.sub.i] are mutually exclusive and exhaustive (in other words, every atomic proposition is true in exactly one i-state, with no two atomic propositions being true in the same i-state), then we can encode the externally visible location counter [L.sub.i] efficiently by setting its value to the name of the proposition that is currently true, rather than the singleton set containing that proposition. That is, if [Q.sub.i] [member of] L[[s.sub.i]] then set [s.sub.i]([L.sub.i]) to "[Q.sub.i]" rather than to {"[Q.sub.i]"}.

5.1 Phase 1

We discuss each step in turn.

Step 1.1: Derive (or Specify) the Initial Kripke Structure. We start with the two-process mutual exclusion specification given in Section 2.4, and apply the CTL decision procedure of Emerson and Clarke [1982] to it. Figure 2 shows the resulting model.

Step 1.2: Replicate Multiple Assignments. This step replicates the assignments x := 2, x := 1 in Figure 2. Figure 9 shows the resulting Kripke structure. The assignment x := 2 which, in Figure 2 is executed only in the [P.sub.1]-transition [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII], is, in Figure 9, executed in every [P.sub.1]-transition starting in a state whose [P.sub.1]-component is [N.sub.1] and ending in a state whose [P.sub.1]-component is [T.sub.1], i.e., the transitions [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII], [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII], [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII], and [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]. x := 1 is similarly replicated. Another point is that every state in Figure 9 assigns a value to x, whereas some states of Figure 2 do not (note our convention in Figure 9, which we use henceforth, of just writing down the value of x, rather than "x = value," as in Figure 2). Thus we see that every state (except [[T.sub.1] x = 2 [T.sub.2]] and [[T.sub.1] x = 1 [T.sub.2]]) in Figure 2 potentially represents two states--one for each element of the domain {1, 2} of x. For example, in Figure 9, [[N.sub.1] [N.sub.2]] has been split into two initial states, [[N.sub.1] 1 [N.sub.2]] and [[N.sub.1] 2 [N.sub.2]].

[FGURE 9 OMITTED]

Step 1.3: Extract a Correct High-Atomicity Program. Figure 10 shows the program extracted from the Kripke structure of Figure 9, using Definition 2.3.

[FIGURE 10 OMITTED]

Step 1.4: Simplify the Guards. Figure 11 illustrates the synchronization skeletons that result when the guards in Figure 10 are simplified. The guard ([N.sub.2] [conjunction] x = 2) [disjunction] ([T.sub.2] [conjunction] x = 1) in [P.sub.1] (from [T.sub.1] to [C.sub.1]) has been simplified to [N.sub.2] [disjunction] x = 1, using the conjunct elimination method of step 1.4. For example, from Figure 9, we see that the condition for replacing ([N.sub.2] [conjunction] x = 2) [disjunction] ([T.sub.2] [conjunction] x = 1) by [N.sub.2] [disjunction] ([T.sub.2] [conjunction] x = 1) is

[[T.sub.1] x = 2 [N.sub.2]] [satisfies] ([N.sub.2] [??] x = 2) and [[T.sub.1] x = 1 [T.sub.2]] [satisfies] ([N.sub.2] [??] x = 2) and [[T.sub.1] x = 2 [T.sub.2]] [satisfies] ([N.sub.2] [??] x = 2) and [[T.sub.1] x = 2 [C.sub.2]] [satisfies] ([N.sub.2] [??] x = 2).

[FIGURE 11 OMITTED]

This is easily verified. In a similar manner, we can then replace [N.sub.2] [disjunction] ([T.sub.2] [conjunction] x = 1) by [N.sub.2] [disjunction] x = 1.

Using the guard elimination method of step 1.4, the guard ([N.sub.2] [conjunction] x = 2) [disjunction] ([N.sub.2] [conjunction] x = 1) [disjunction] ([T.sub.2] [conjunction] x = 1) [disjunction] ([C.sub.2] [conjunction] x = 1) in [P.sub.1] in Figure 10 has been replaced by true. Likewise, the guard ([N.sub.2] [conjunction] x = 2) [disjunction] ([T.sub.2] [conjunction] x = 1) in [P.sub.1] (from [C.sub.1] to [N.sub.1]) has been simplified to true. The program resulting from all of these guard simplifications (applied symmetrically to [P.sub.2] as well) is shown in Figure 11.

5.2 Phase 2

We discuss each step in turn.

Step 2.1: Introduce the Externally Visible Location Counters. Figure 12 shows the program of Figure 11 after the externally visible location counters [L.sub.1] and [L.sub.2] have been introduced. Note that we have used the convention (mentioned at the beginning of Section 5) of writing [L.sub.i] -- "[Q.sub.i]" instead of [Q.sub.i] [member of] [L.sub.i] when [s.sub.i]([L.sub.i]) assigns true to exactly one proposition. This convention is used in the sequel for the mutual exclusion example (but we abuse notation slightly by omitting the quotation marks around the atomic proposition names).

[FIGURE 12 OMITTED]

Step 2.2: Decompose the Test-and-Set Arcs, and Step 2.3: Decompose the Multiple-Writing Arcs and Number the Local States. Figure 13 shows the program of Figure 12 after all arcs have been decomposed. Note that the arc labeled x := 2//[L.sub.1] := [T.sub.1] has been decomposed into two sequences, each sequence corresponding to one of the two possible serializations of the two write operations x := 2 and [L.sub.1] := [T.sub.1].

[FIGURE 13 OMITTED]

In Figure 13, there are three local states in the skeleton for [P.sub.1] with the same atomic proposition valuation: they all assign false, true, false to [N.sub.1], [T.sub.1], [C.sub.1] respectively (these states being shown as circles containing [T.sub.1], as per our convention for figures). To distinguish local states with the same atomic proposition valuation, we now number the local states, as discussed in Section 3.2. Figure 14 shows the result of performing this numbering on the program in Figure 13. The numbers are shown as superscripts on the atomic proposition(s) displayed in each local state. We use this convention of superscripting all the displayed atomic propositions of a local state with the number of that local state.

[FIGURE 14 OMITTED]

5.3 Phase 3

Figure 15 shows (part of) the global-state transition diagram of the program in Figure 14. The solid lines indicate paths that correspond to (decompositions of) paths in Figure 9. These paths represent the same interleavings of transitions as in Figure 9. The single-dashed path shown represents a "new" interleaving, due to the decomposition of the arcs (of the program in Figure 12). There are many more such new paths, but they have been omitted for sake of clarity of the figure. Also, the assignments to [L.sub.1], [L.sub.2] have been omitted, since they can be easily inferred from the begin and end states of each transition.

[FIGURE 15 OMITTED]

5.4 Phase 4

We discuss each step in turn.

Step 4.1: Label the Reachable States. Taking as our specification that given for the two-process mutual exclusion problem in Section 2.4, we see, that in Figure 15, every state will be labeled with [logical not]([C.sub.1] [conjunction] [C.sub.2]). Also, all states satisfying [T.sub.1] ([T.sub.2]) will be labeled with [AFC.sub.1] ([AFC.sub.2]) respectively.

Step 4.2: Prune Structure So that Labels Are Satisfied. Figure 15 contains a state s = [[C.sup.1.sub.1] 2 [C.sup.1.sub.2]] (at the end of the dashed path) such that [logical not] ([C.sub.1] [conjunction] [C.sub.2]) [member of] label(s), and s [??] [logical not]([C.sub.1] [conjunction] [C.sub.2]). Hence, by the Prop-rule, s must be made unreachable. A deletable transition along a path from an initial state to s is [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]. Since this transition is a member of an unguarded family, the entire family must be deleted. Figure 16 shows (part of) the resulting Kripke structure. Again, there is a state t (in Figure 16) such that [logical not]([C.sub.1] [conjunction] [C.sub.2]) [member of] label(t), and t [??] [logical not]([C.sub.1] [conjunction] [C.sub.2]), and so t must be made unreachable by the Prop-rule. This can be achieved by the deletion of the (unguarded) family containing the transition [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]. The (reachable part of the) complete Kripke structure that results after all deletions have been made is shown in Figure 17.

[FIGURES 16-17 OMITTED]

5.5 Phase 5

We discuss each step in turn.

Step 5.1: Ensure Atomic Read/Write Form. Figure 17 gives M"' for our extended example. There is exactly one guarded and nonwriting [P.sub.1]-family F in M"', consisting of the following transitions:

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

We can verify, by inspection, that this family is single-reading. The single [P.sub.2]-family in M"' that is guarded and nonwriting is also seen to be single-reading. Thus, the function CHECK-STRUCTURE returns true, and so no states need be deleted.

Step 5.2: Extract the Final Atomic Read/Write Program. Consider first the guarded and nonwriting [P.sub.1]-family F in M"', given above. The only simple terms that do not generate transitions outside F are "[N.sub.2] [member of] [L.sub.2]" and "x = 1." Thus, in the invocation CHECK-FAMILY(M"', F), ok is set to {"[N.sub.2] [member of] [L.sub.2]", "x = 1"}. Since "[N.sub.2] [member of] [L.sub.2]" generates [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII], and "x = 1" generates [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII], we see that COV(F, ok) is true in this case. Hence, CHECK-FAMILY(M"', F) computes the guard "[N.sub.2] [member of] [L.sub.2] [disjunction] x = 1" for the corresponding extracted arc (this is returned as the final value of F.srguard). Thus the single-reading arc ([T.sup.2.sub.1], [N.sub.2] [member of] [L.sub.2] [disjunction] x = 1 [right arrow]. skip, [T.sup.3.sub.1) is extracted.

The unguarded [P.sub.1]-families in Figure 17 and the corresponding extracted arcs are as follows:

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

from which the unguarded arc ([N.sup.1.sub.1], true [right arrow] [L.sub.1] := {T1},[T.sup.1.sub.1) is extracted, and

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

from which the unguarded arc ([T.sup.1.sub.1], true [right arrow] x := 2, [T.sup.2.sub.1]) is extracted, and

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

from which the unguarded arc ([T.sup.3.sub.1], true [right arrow] [L.sub.1] := {[C.sub.1]}, [C.sup.1.sub.1]) is extracted, and

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

from which the unguarded arc ([C.sup.1.sub.1], true [right arrow], [L.sub.1] := {[N.sub.1]}, [N.sup.1.sub.1]) is extracted.

These extracted arcs constitute the synchronization skeleton for [P.sub.1] in Figure 18. The synchronization skeleton for [P.sub.2], also shown in this figure, is extracted from the Kripke structure of Figure 17 in a similar manner. Figure 18 gives the synthesized atomic read/write program for our extended example: the two-process mutual exclusion problem. Note that we use the convention given in the beginning of Section 5.

[FIGURE 18 OMITTED]

5.6 Comparison with Peterson's Mutual Exclusion Solution

It is instructive to compare our synthesized solution to the two-process mutual exclusion problem, given in Figure 18, with the well-known solution of Peterson [1981], which is shown in Figure 19. [s.sub.1], [t.sub.1], [u.sub.1], [v.sub.1] ([s.sub.2], [t.sub.2], [u.sub.2], [v.sub.2]) are names for local states of [P.sub.1] ([P.sub.2]) respectively, [s.sub.1], [s.sub.2] are the noncritical states, and [v.sub.1], [v.sub.2] are the critical states.

[FIGURE 19 OMITTED]

We see that TURN plays the same role as x, with "flipped" values, so that TURN = 2 gives priority to [P.sub.1], whereas x = 1 gives priority to [P.sub.1]. We also see that Q1 is a boolean variable that indicates whether or not [P.sub.1] is in its neutral state, i.e., Q1 = false is "equivalent" to [N.sub.1] = true. We note that Peterson's solution only has four local states in each process, whereas ours has five (with one binary-valued shared variable in both solutions). This is explained by noting that our synthesis method is suboptimal in the following respect. Inspecting Figure 11, we note that the only atomic proposition in [AP.sub.2] = {[N.sub.2], [T.sub.2], [C.sub.2]} that is tested by [P.sub.1] is [N.sub.2]. In other words, [N.sub.2] is the only atomic proposition that needs to be "externally visible." The propositions [T.sub.2] and [C.sub.2] are not tested by [P.sub.1] and so do not have to be externally visible. Thus, we could optimize the synthesis method by "grouping" only the atomic propositions of each process [P.sub.i] that are referenced by some [P.sub.j], j [not equal to] i, into the externally visible location counter [L.sub.i]. The remaining propositions could then be grouped into an internal location counter [IL.sub.i]. In the mutual exclusion example, we see that [L.sub.2] ([L.sub.1]) would incorporate just [N.sub.2] ([N.sub.1]) respectively, while [IL.sub.2] ([IL.sub.1]) would incorporate [T.sub.2] ([T.sub.1]) and [C.sub.2] ([C.sub.1)] respectively. Thus, for example, the arc ([T.sub.2], [N.sub.1] [disjunction] x = 2 [right arrow] skip, [C.sub.2]) in Figure 11 becomes, upon introduction of the location counters, the arc ([T.sub.2], [L.sub.1] = [N.sub.1] [disjunction] x = 2 [right arrow] [IL.sub.2] := [C.sub.2], [C.sub.2]), cf. Figure 12. Since [IL.sub.2] is not externally visible, a write operation to it does not count as a write to shared data, and so, in the decomposition step of Phase 2, the arc ([T.sub.2], [L.sub.1] = [N.sub.1] [disjunction] x = 2 [right arrow] [IL.sub.2] := [C.sub.2], [C.sub.2]) can be left as is, and considered to be a guarded and nonwriting arc, whereas the analogue arc in Figure 12, namely ([T.sub.2], [L.sub.1] = [N.sub.1] [disjunction] x = 2 [right arrow] [L.sub.2] := [C.sub.2], [C.sub.2]), has to be decomposed into the guarded and nonwriting arc ([T.sub.2], [L.sub.1] = [N.sub.1] [disjunction] x = 2 [right arrow] skip, [T.sub.2]), followed by the unguarded and single-writing arc ([T.sub.2], true [right arrow] [L.sub.2] := [C.sub.2], [C.sub.2]), cf. Figure 13. Avoiding this decomposition would result in a mutual exclusion program with four local states per process, which would be effectively isomorphic to Peterson's program.

Since this optimization is straightforward in principle, and does not add any important capabilities to our method, we omit it for sake of simplicity.

5.7 Another Example: The Barrier Synchronization Problem

In this problem, each process consists of a cyclic sequence of two terminating phases, phase A and phase B. Process i (i [member of] {1, 2}) is in exactly one of four local states, [SA.sub.i], [EA.sub.i], [SB.sub.i], [EB.sub.i], corresponding to the start of phase A, the end of phase A, the start of phase B, and the end of phase B, respectively. The CTL specification is the conjunction of the following:

(1) Initial State (both processes are initially at the start of phase A): [SA.sub.1] [conjunction] [SA.sub.2]

(2) The start of phase A is immediately followed by the end of phase A: AG([SA.sub.i] [??] [AY.sub.i][EA.sub.i])

(3) The end of phase A is immediately followed by the start of phase B: AG([EA.sub.i] [??] [AY.sub.i][SB.sub.i])

(4) The start of phase B is immediately followed by the end of phase B: AG([SB.sub.i] [??] [AY.sub.i][EB.sub.i])

(5) The end of phase B is immediately followed by the start of phase A: AG([EB.sub.i] [??] [AY.sub.i][SA.sub.i])

(6) [P.sub.i] is always in exactly one of the states [SA.sub.i], [EA.sub.i], [SB.sub.i], [EB.sub.i]: AG([SA.sub.i] [equivalent to] [logical not] ([EA.sub.i] [disjunction] [SB.sub.i] [disjunction] [EB.sub.i])) [conjunction] AG([EA.sub.i] [equivalent to] [logical not] ([SA.sub.i] [disjunction] [SB.sub.i] [disjunction] [EB.sub.i])) [conjunction] AG([SB.sub.i] [equivalent to] [logical not] ([SA.sub.i] [disjunction] [EA.sub.i] [disjunction] [EB.sub.i])) [conjunction] AG([EB.sub.i] [equivalent to] [logical not] ([SA.sub.i] [disjunction] [EA.sub.i] [disjunction] [SB.sub.i]))

(7) [P.sub.1] and [P.sub.2] are never simultaneously at the start of different phases: AG([logical not]([SA.sub.1] [conjunction] [SB.sub.2])) [conjunction] AG([logical not]([SA.sub.2] [conjunction] [SB.sub.1]))

(8) [P.sub.1] and [P.sub.2] are never simultaneously at the end of different phases: AG([logical not]([EA.sub.1] [conjunction] [EB.sub.2])) [conjunction] AG([logical not]([EA.sub.2] [conjunction] [EB.sub.1]))

(9) A transition by one process cannot cause a transition by another, i, j [member of] {1, 2}, i [not equal to] j (interleaving model of concurrency):

AG([SA.sub.i] [??] [AY.sub.j][SA.sub.i]) [conjunction] AG([EA.sub.i] [??] [AY.sub.j][EA.sub.i]) [conjunction] AG([SB.sub.i] [??] [AY.sub.j][SB.sub.i]) [conjunction] AG([EB.sub.i] [??] [AY.sub.j][EB.sub.i])

(10) It is always the case that some process can move: AGEXtrue

(7) and (8) together specify the synchronization aspect of the problem: [P.sub.1] can never get one whole phase ahead of [P.sub.2] (and vice-versa). Figure 20 presents the program synthesized by the Emerson and Clarke [1982] method from the barrier synchronization specification. Figure 21 presents the atomic read/write program synthesized from this specification by our synthesis method.

[FIGURE 20-21 OMITTED]

6. TRANSLATING SYNCHRONIZATION SKELETON PROGRAMS INTO PROGRAMS THAT USE ATOMIC REGISTERS

Our current model of computation admits arcs that read or write an externally visible variable (either [L.sub.i] or a shared variable) and simultaneously modify a local variable, namely the variable encoding the local-state numbering function num. Hence, strictly speaking, we are not adhering to a single atomic read/single atomic write model of computation, which allows a single atomic read or write operation at a time, whether of a local or a shared variable. Also, the synchronization skeleton model is really based upon the use of an await primitive to evaluate guards that reference nonlocal variables: the arc ([s.sub.i], B [right arrow] skip, [t.sub.i]) is essentially the same as an "await B" statement. The await primitive is generally regarded as a higher-level primitive than atomic reads and writes of registers. This is because implementation of an await involves busy waiting: the nonlocal variables referenced in the await have to be read repeatedly until the await condition becomes true (if ever). Thus, as long as the await condition is false, the nonlocal variables are being read, but these read operations are "hidden" in that they are not reflected in the transitions generated by the program containing the await--the await either occurs atomically or not at all. We now present a method of translating the synthesized synchronization skeleton programs into programs that use n-bit atomic registers [Singh et al. 1994] to implement all variables that are accessed by more than one process. We proceed as follows.

Each process [P"'.sub.i] of P"' is implemented as a single do statement [D.sub.i] (in Dijkstra's guarded command language [Dijkstra 1976]). We make no assumptions about the level of atomicity of the implementation of guarded commands, e.g., the evaluation of guards is not necessarily atomic--it can, for example, be a sequence of operations, which first reads all the referenced variables, and then evaluates the guard. Associated with each [D.sub.i] are the variables [L.sub.i] and [num.sub.i]. [L.sub.i] is the externally visible location counter, and [num.sub.i] is an integer variable that contains the number of the current i-state. [L.sub.i] is readable (but not writable) by [D.sub.j], j [not equal to] i, and [num.sub.i] is local to [D.sub.i], i.e., not readable or writable by any [D.sub.j], j [not equal to] i. Additionally, we introduce a (local to [D.sub.i]) variable [LL.sub.i]. [LL.sub.i] keeps track of the externally visible variable [L.sub.i], so that we avoid making two references to externally visible variables in a single guarded command (this is necessary for technical reasons). Finally, we also have the shared variables in SH, which are shared by all [D.sub.i], i [member of] [1 : K].

To emphasize the atomic registers model, we use read, write to indicate read and write operations on nonlocal variables (i.e., variables that are visible to more than one [D.sub.i], i [member of] [1 : K], that is, the shared variables in SH and the [L.sub.i], i [member of] [1 : K]). Each [L.sub.i], i [member of] [1 : K], is implemented by a multiple-reader, single-writer, n-bit atomic register, and each x [member of] SH is implemented by a multiple-reader, multiple-writer, n-bit atomic register [Singh et al. 1994].

The guarded commands of each [D.sub.i] are derived as follows.

--An unguarded and single-writing arc in [P.sub.i] gives rise to a single guarded command. There are two cases, depending on the form of the arc.

(1) If the arc has the form ([s.sub.i], true [right arrow] x := c, [t.sub.i]), then the corresponding guarded command is

[LL.sub.i] = L[[s.sub.i]] [conjunction] [num.sub.i] = num([s.sub.i]) [right arrow] write(x,c); [num.sub.i] := num([t.sub.i]).

(2) If the arc has the form ([s.sub.i], true [right arrow] [L.sub.i] := L[[t.sub.i]], [t.sub.i]), then the corresponding guarded command is

[LL.sub.i] = L[[s.sub.i]] [conjunction] [num.sub.i] = num([s.sub.i]) [right arrow] write([L.sub.i], L[[t.sub.i]]); [LL.sub.i] := L[[t.sub.i]]; [num.sub.i] := num([t.sub.i]).

--A single-reading and nonwriting arc [AR.sub.i] = ([s.sub.i], [V.sub.k[member of][1:n]] [b.sub.k] [right arrow] skip, [t.sub.i]) in [P"'.sub.i] gives rise to n guarded commands, one guarded command for each k in [1 : n], as follows. We introduce a local variable [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] (unique to [AR.sub.i]), which is a counter modulo n. Its purpose is to ensure that every disjunct of [V.sub.k[member of][1:n]] [b.sub.k] is tested for truth, so that if [V.sub.k[member of][1:n]] [b.sub.k] is continuously true, then this is eventually detected. We also introduce a local boolean variable [Lb.sub.i] (unique to [P"'.sub.i] used to temporarily store the "sampled" value of [b.sub.k]. For each k in [1 : n], we have the following guarded command in [D.sub.i]
[LL.sub.i] = L[[s.sub.i]] [conjunction]
[num.sub.i] = num([s.sub.i]) [conjunction]
ctr = k [right arrow] [Lb.sub.i] := eval([b.sub.k]);
                      if [Lb.sub.i] [right arrow]
                      [num.sub.i] := num([t.sub.i])
                      [??] [logical not] [Lb.sub.i] [right arrow]
                      ctr := (k mod n) + 1
                      fi.


The function eval, whose purpose is to return the value of a simple term in the current global state, is given below. It takes a simple term as argument, reads the shared variable or externally visible location counter in the term, and then returns the value of the term.
boolean function eval(b)
/ b is assumed to be either a simple term, or the constant true
[TLL.sub.i], [Lx.sub.i] are local variables unique to [P"'.sub.i] */

if b [??] "[Q.sub.j] [member of] [L.sub.j]"
[right arrow] [TLL.sub.i] := read ([L.sub.j]);
              return ([Q.sub.j] [member of] [TLL.sub.i])
[] b [??] "x = c"
[right arrow] [Lx.sub.i] := read(x);
              return ([Lx.sub.i] = c)
[] b [??] "true" [right arrow] return (true)
fi


In practice, eval is most efficiently implemented as an in-line macro. The tests on the syntactic form of b (b [??] "[Q.sub.j] [member of] [L.sub.j]", b [??] "x = c", b [??] "true") can then be dispensed with. It is, however, technically convenient for our purposes to use eval to encapsulate all the read operations.

The translation of P"' = [P"'.sub.1][parallel] ... [parallel][P"'.sub.K] into guarded command notation is then given by D = [D.sub.1] [parallel] ... [parallel][D.sub.K], where each [D.sub.i], i [member of] [1 : K], is the translation of [P"'.sub.i] given above, and [parallel] still denotes parallel composition under a nondeterministic interleaving model of concurrency. Figure 22 shows the result of applying this translation to the program of Figure 18.

[FIGURE 22 OMITTED]

Let D = [D.sub.1] [parallel] ... [parallel] [D.sub.K] be a large-grain version of D in which the execution of each guarded command is atomic, that is, the computations of D are sequences of segments, each segment consisting entirely of all of the operations resulting from a single execution of a single guarded command. Let [M.sup.D] = ([S.sup.D.sub.0], [S.sup.D], [R.sup.D]), [M.sup.D] = ([S.sup.D.sub.0], [S.sup.D], [R.sup.D]) be the global-state transition diagrams generated by the execution of D, D respectively (the formal definitions of [M.sup.D], [M.sup.D] are similar to the global-state transition diagram definition (2.2.2), and are a straightforward exercise in operational semantics). A global state u of D (or D) is a mapping of the variables of D onto their appropriate domains. [S.sup.D] is the set of all such global states. [S.sup.D] is the set of all such global states that assign the same values to [L.sub.i] and [LL.sub.i] for all i [member of] [1 : K].

Define an empty transition of [M.sup.D] to be a transition of [M.sup.D] in which the eval function is invoked, and returns false. Thus an empty transition tests a disjunct of some guard in some process [P"'.sub.i] and finds it false, and so no [P"'.sub.i]-transition is "simulated" by [D.sub.i]. It is possible, therefore, to have fullpaths with a suffix consisting entirely of (the interleaved operations of) empty transitions, which means that no real progress in the computation of P"' is being made. The only thing that is occurring is that the same false guards are being tested over and over again. (19) Likewise, define an empty transition of [M.sup.D] to be a transition of [M.sup.D] resulting from an execution of the eval function which returns false (recall that in [M.sup.D] there will be several transitions resulting from a single execution of eval, whereas in [M.sup.D], execution of eval induces exactly one transition, i.e, there is a one-to-one correspondence).

We therefore impose the following progress condition on the interleaving of operations of the [D.sub.i] (in both [M.sup.D] and [M.sup.D]).

Progress Condition. No fullpath of [M.sup.D], [M.sup.D] has a suffix composed entirely of empty transitions.

The progress condition is a restriction only on the infinite behavior of [M.sup.D], [M.sup.D]--it cannot be violated by any finite prefix of some path in [M.sup.D,] [M.sup.D]. In form, therefore, it resembles a fairness notion [Francez 1986]. Its sole purpose is to rule out infinite paths in which (one or more) false guards in P"' are tested continuously from some point onward.

The following theorem presents our main correctness result for the atomic-registers-based implementation. It essentially states that the guarded command implementation D satisfies the original problem specification (with the local structure specifications appropriately modified).

THEOREM 6.1 (SOUNDNESS THEOREM FOR REGISTERS MODEL). If [S.sup.D.sub.0] [not equal to] [??]), and f is a conjunct of the given specification, and the progress condition holds, then D is an atomic registers program that satisfies [f.sup.*], where [f.sup.*] = f if f has one of the forms h, AGh, AG(p [??] A[q[union]r]), and [f.sup.*] = AG([p.sub.i] [??] [EX.sub.i]([p.sub.i] disjunction] [q.sub.i])), AG([p.sub.i] [??] [AY.sub.i]([p.sub.i] [disjunction] [q.sub.i])) if f = AG([p.sub.i] [??] [EX.sub.i][q.sub.i]), AG([p.sub.i] [??] [AY.sub.i][q.sub.i]) respectively, and where p, q, r, h [member of] LO(AP, [logical not], conjunction]), [p.sub.i], [q.sub.i] [member of] LO([AP.sub.i], [logical not], [conjunction]).

The proof is omitted due to lack of space, and can be found in [Attie 1995]. Essentially, we show that [M.sup.iv] and [M.sup.D] agree on all CTL formulae of the form [f.sup.*], and so do [M.sup.D] and [M.sup.D]. The relation between [M.sup.iv] and [M.sup.D] is established by showing that there is a one-to-one correspondence between a transition in [M.sup.iv] that arises from the execution of some arc [AR.sub.i] of P"', and the transition in [M.sup.D] that arises from the execution of the guarded command in D that is derived from [AR.sub.i]. This establishes a bisimulation between [M.sup.iv] and [M.sup.D], from which it follows that [M.sup.iv] and [M.sup.D] satisfy the same CTL formulae [Browne et al. 1988]. The relation between [M.sup.D] and [M.sup.D] is established by using the results of Lamport [1990], which shows that under certain conditions a class of correctness properties is preserved when a sequence of actions is combined into a single atomic action (provided that the sequence contains only a single access to a single shared variable), or the atomic action is decomposed into the sequence. The main result of Lamport [1990] then implies that [M.sup.D] and [M.sup.D] agree on all formulae in our specification language. The reader is referred to Attie [1995] for details of the proof.

Applying Proposition 4.5.2.1 then allows us to conclude that D satisfies [f.sup.*]. Furthermore, D is an atomic registers program by construction of the translation procedure from synchronization skeleton notation given above.

6.1 Implementing the Progress Condition

We now show that implementing the progress condition does not unduly restrict the scheduling of D.

Claim. Let u be an arbitrary reachable state in [M.sup.D,] and let [[pi].sup.D] be an arbitrary maximal path of [M.sup.D] starting in u. Then there exists a state v along [[pi].sup.D], and a guarded command GC in D, such that v(GC.guard) = true, and execution of GC in v results in a nonempty transition.

A proof of this claim is provided in Attie [1995].

Thus, we see that implementing the progress condition does not restrict the scheduling of D (except to prohibit infinite empty paths), since, from any reachable state, no matter which path is chosen by the scheduler, it will always be possible to satisfy the progress condition, i.e., to eventually execute a nonempty transition.

In practice, the progress condition could be implemented by adding to each [D.sub.i] a variable flag--[empty.sub.i], which would be set to true whenever eval returns false, and set to false whenever eval returns true or a write is executed. The scheduler would then check for states in which [[conjunction].sub.i[member of][1:K]] flag--[empty.sub.i] is true. All that is required is to attempt to detect [[conjunction].sub.i[member of][1:K]] flag--[empty.sub.i] under the assumption that it is eventually stable. In the event of detection, the scheduler must intervene, but may wait arbitrarily long to do so. Intervention takes the form of finding an enabled guarded command whose execution leads to a nonempty transition, (from the claim, there must be at least one such guarded command) and executing it.

7. ANALYSIS AND DISCUSSION

7.1 Space Complexity

Consider the finite-state model which is input to Phase 1. M is either given directly, as input to our synthesis method, or is generated by the synthesis method of Emerson and Clarke [1982], from a CTL specification. In the case that M is generated by the Emerson and Clarke [1982] method, a shared variable is introduced whenever two or more global states occur that are propositionally equivalent, but not temporally equivalent in the sense that they differ in some of the temporal formulae that they satisfy (see Section 2.6). The shared variable serves to distinguish such states from each other. We shall assume that a directly given M also has this characteristic. This is a reasonable assumption, since states that are propositionally inequivalent can always be distinguished by reading the externally visible location counters (which encode the values of the atomic propositions), and so no shared variable is needed to distinguish these states from each other. In the worst case, the number of sets of propositionally equivalent but temporally inequivalent states is linear in the size of M, and therefore so is the number of shared variables. Hence, the refinement of the model M effected by Phases 1 and 2 can lead to an exponential blowup, causing the method to have (at least) double-exponential space complexity. To avoid this, we note that any finite-state model M can be easily modified so that it uses at most one shared variable.

Let [bar]s, [bar]t denote different sets of propositionally equivalent but temporally inequivalent global states in M. Let [x.sub.s], [x.sub.t] denote the shared variables that are introduced to distinguish all the occurrences of global states in [bar]s, [bar]t respectively. [x.sub.s] is written only upon entry to states in [bar]s and read only upon exit from states in [bar]s, likewise for [x.sub.t.] Since [bar]s and [bar]t have no common members (by definition), it should be possible to "reuse" [x.sub.s] to distinguish among the global states in [bar]t. Even in the case where there is a transition from a state in [bar]s to a state in [bar]t this would work: the transition would be labeled with a test (to determine which state in [bar]s is in fact the current global state) and set (to record which global state in [bar]t is being entered). We refer the reader to Emerson and Clarke [1982] for more discussion of this technique, while also noting that it is applicable to directly given models M, as well as those generated by the Emerson and Clarke [1982] synthesis method.

With only one shared variable present, we see that once all atomic propositions of a process have been consolidated into the externally visible location counter, then the largest multiple-assignments that could occur would have size two. Hence, in the decomposition carried out in Phase 2, each local state can be refined into at most five local states (with the same propositional valuation but different local state numbers--see Section 3.2). This is because one new local state is introduced for the "test," and three new local states are introduced for the two serializations of the multiple-assignment.

Suppose that the high-atomicity program extracted from M in Phase 1 has K processes with O(N) local states each. By Definition 2.3, every local state in (some process [P.sub.i] of) the program is the projection onto [P.sub.i] of some global state in M. Thus, M contains O([N.sup.K]) states. By the previous paragraph, in any intermediate program generated by the method, (including the final atomic read/write program), there are K processes each containing O(5N) local states, i.e., O(N) local states. Thus, the largest intermediate global-state transition diagram generated by our method contains O([N.sup.K]) states. Thus, our method has space complexity O([N.sup.K]), i.e., the same order of (space) complexity as the finite-state model M that is input to the method. This is clearly the best that we can do.

7.2 Related Work

The refinement of concurrent programs is a topic of extensive research, with many proposed approaches. The most general approach constructs a low-atomicity program directly, and then establishes that the low-atomicity program is a "correct implementation" of the high-atomicity program. Different approaches are distinguished by their notion of "correct implementation." For example, in the I/O automaton approach [Lynch and Tuttle 1987; Lynch and Vaandrager 1995], a low-atomicity program is a correct implementation if each of its externally observable behaviors (traces) is also a trace of the high-atomicity program. The approach of Back and von Wright [1994] for refinement of action systems is likewise based on trace-inclusion. The proofs of correct implementation are based on exhibiting a simulation relation between the low-atomicity and high-atomicity programs. Simulation is also used to establish refinement in the refinement calculus [Back 1989]. In UNITY [Chandy and Misra 1988], refinement is performed on specifications, expressed as UNITY formulae, and a refined specification is correct if it logically implies the higher-level specification.

In some approaches, the low-atomicity program is shown to have some properties that are derived from properties established for the high-atomicity program. (Our method uses a similar idea for the local-structure properties AG([p.sub.i] [??] [EX.sub.i][q.sub.i]) and AG([p.sub.i] [??] [AY.sub.i][q.sub.i])--see Theorems 4.5.2.2 and 6.1.) Manna and Pnueli [1995, Chapter 1] shows how an invariant for the low-atomicity program can be derived as a refinement itself of an invariant for the high-level program. Other methods for refining a high-atomicity program together with its invariant are given in Gribomont [1990], Gribomont [1993]. Here, each time the program is refined, the invariant that holds for the refined program is derived systematically from the original program, the refined program, and the invariant that holds for the original program.

While some of the above methods provide a methodology for deriving the low-atomicity program from the high-atomicty one, there is little guidance as to which choices of refinement step will provide a correct refinement. This usually has to be established afterward, e.g., by attempting to construct a simulation relation, or a proof of invariance. Our method provides an initial "naive" refinement, in which all possible refinements of each process action are performed initially. Then, our method provides guidance in eliminating refinements that cause the specification to be violated (see the deletion rules, Figure 7).

The only other temporal logic synthesis method to date that we are aware of which generates atomic read/write programs is that of Dill and Wong-Toi [1990] for synthesizing reactive modules. This method has double-exponential space complexity in the length of the specification, and produces a program that has size double-exponential in the length of the specification. By comparison, our method has single-exponential space complexity in the length of the specification. Furthermore, while the programs we synthesize could in the worst case have length exponential in the specification, this would occur only if one process was much larger than the others, since the size of the (exponentially large) model is on the order of the product of the sizes of the processes. Thus, in practice, we expect our programs to have size polynomial in the length of the specification.

On the other hand, the method of Dill and Wong-Toi [1990] is complete whereas ours is not. While interesting theoretically, this advantage of Dill and Wong-Toi [1990] is unlikely to have practical significance because the double-exponential space complexity is a considerable impediment to practical application.

7.3 Further Directions for Research

Our method may easily be extended to handle temporal modalities other than those given in Section 2.4. All that is needed is to devise the appropriate labeling and deletion rules for Phase 4. All the other phases of the method are independent of the particular subset of CTL chosen as the specification language. Furthermore, it may be possible to extend our method to synthesize shared-memory concurrent programs for different synchronization primitives such as compare-and-swap, fetch-and-add, or n-register assignment [Herlihy 1991]. The main step would be devising a characterization of the Kripke structures corresponding to programs containing the particular primitive, much like our atomic read/write Kripke structures correspond to atomic read/write programs. The refinement phases (1 and 2) would then have to be modified to refine the initial model into a structure that (after the deletion rules have been applied) is in the appropriate form.

One potential drawback of our method is its susceptibility to state-explosion. Our method requires generation of the global-state transition diagram. For a program consisting of K processes each with O(N) local states, the size of the global-state transition diagram is O([N.sup.K]). State-explosion can be dealt with by integrating our work here with that of Attie and Emerson [1998], Attie [1999]. In that method, construction of the exponentially large global-state transition diagram is avoided. Instead, it constructs a state transition diagram for each pair of component processes (of the program) that interact (call these neighbors). This reduces the space complexity to O([K.sup.2][N.sup.2]). A "pair-program," which embodies all the interactions of the two processes, is then extracted from this state transition diagram. These pair-programs are then composed in a certain way to generate the final program. Integrating the two methods will result in a method that can synthesize large atomic read/write programs efficiently. There are some nontrivial issues however. For example, the composition of the pair-programs relies on a process being able to interact in one atomic step with all of its neighbors. This high atomicity will have to be refined in some way, in the combined method.

Another possible extension of our work would deal with synthesizing fault-tolerant programs. We have already devised a method [Arora et al. 1998] for synthesizing fault-tolerant programs using high-atomiciy operations. Integrating this with our work here would allow the synthesis of fault-tolerant atomic read/write programs, or more generally, fault-tolerant programs that use synchronization primitives such as compare-and-swap. In particular, by specifying that all but one process can crash, we could deal with the important case of synthesizing wait-free programs.

7.4 Conclusions

We have presented a method for the synthesis of atomic read/write programs from specifications expressed in temporal logic. The method is sound but not complete. Although automatic in principle, some of the steps involved require a large amount of search. For example, in the deletion step of Phase 4, there are in general many choices of transitions to be deleted. Thus the method may be best implemented as an interactive tool, akin to a theorem prover, allowing human guidance in order to cut down on the search. Designing good heuristics for selecting transitions for deletion is a topic for future work.

A shortcoming of our method is its incompleteness. This incompleteness arises because our method starts from a coarse high-level program that embodies a particular solution to the specified problem. While this particular solution may be realizable using high-atomicity primitives, it may not be realizable using atomic reads and writes. On the other hand, there may be other solutions to the problem (essentially different from the particular high-level program that our method starts with) which may be realizable using atomic reads and writes. Another way of saying this is that our method embodies one particular strategy for refining a progam from high-level atomicity to atomic read/write atomicity. Other strategies are possible, and these might generate solutions that our method would miss.

A complete method would have a wider scope of applicability. Extending the method to make it complete is thus of some interest. On the other hand, completeness is not essential to practical applicability, as our synthesis of Peterson's solution shows.

Recall that given a specification consisting of a finite-state machine M and CTL formula f, it is not necessary that M, [S.sub.0] [satisfies] f ([S.sub.0] is the set of initial states of M), since the method deletes any states/transitions that cause a violation of f. In the "normal" refinement scenario where M, [S.sub.0] [satisfies] f, states/transitions that cause a violation of f can only be introduced by the decomposition step (Phase 2). However, if M, [S.sub.0] [not satisfies] f, then such states/transitions could be present initially. In this case, we can regard the synthesis method as providing both refinement and debugging.

The work presented in this paper is one building block in our research program, which aims to create truly practical synthesis methods. We have now devised methods that each deal with one aspect of realistic concurrent programs: a realistic, low-atomicity model of concurrent computation (this paper), state-explosion [Attie and Emerson 1998; Attie 1999], and fault-tolerance [Arora et al. 1998]. Some other topics to be dealt with are real-time, and synthesis of asynchronous message-passing distributed programs. The ultimate goal is to create a toolkit of synthesis methods that address many issues in the derivation of large, complex, distributed systems from formal specifications.

APPENDIX

A. PROOFS

PROOf OF LEMMA 3.4.3. The proof is by double implication.

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] follows from [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]. Let [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] be an arbitrary [P.sub.i]-transition in [R.sup.2]. Hence, by the global-state transition diagram definition (2.2.2), there is some arc A[R.sub.i]= (s [up arrow] i, B [right arrow] A, t [up arrow] i) in [P.sub.i] such that s(B) = true. By Proposition 3.4.2 and the atomic read/write program definition (3.1.4), A[R.sub.i] is either single-reading and nonwriting, or unguarded and single-writing. Thus there are two cases.

Case 1: A[R.sub.i] is unguarded and single-writing. By Definition 3.4.1, there must be an unguarded and single-writing [P.sub.i]-family F in M such that F.start = s [up arrow] i, F.finish = t [up arrow] i, F.assig = A. So, by the unguarded family definition (3.3.2), [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII], for some state u such that u [up arrow] i = F.finish. (End of case 1.)

Case 2: A[R.sub.i] is guarded and nonwriting. By Definition 3.4.1, there must be a guarded and nonwriting [P.sub.i]-family F in M such that F.start = s [up arrow] i and F.finish = t [up arrow] i. Also B, the guard of A[R.sub.i], is, by Definition 3.4.1 and Definition 3.3.3, [[V].sub.k[member of][1:n]] [b.sub.k], where [U.sub.k[member of][1:n]] [F.sub.k], and conditions (G1), (G2) of Definition 3.3.3 are satisfied. We showed above that s(B) = true. Hence s([b.sub.l]) = true for some l [member of] [1 : n]. Since, by assumption, s is reachable in M, we can instantiate (G2) for state s, and then take the contrapositive, which yields

if s([b.sub.l]) = true then s is the start state of some transition in [F.sub.l].

Since [F.sub.l] [subset or equal to] F, we have [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] for some state u such that u [up arrow] i = F.finish. (End of case 2.)

Thus in both cases, [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] for some state u such that u [up arrow] i = F.finish. By the assumption on Kripke structures in Section 2.3, we have

(a) <s [up arrow] SH> A <u [up arrow] SH> and [for all]j [member of] [1 : K] - {i}, s [up arrow] j = u [up arrow] j.

Also in both cases, [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] (by assumption) and t [up arrow] i = F.finish. By the global-state transition diagram definition (2.2.2), we have

(b) <s [up arrow] SH> A <t [up arrow] SH> and [for all]j [member of] [1 : K] - {i}, s [up arrow] j = t [up arrow] j.

Since A is either skip or a deterministic multiple assignment, we have, from the Hoare triples in (a) and (b), u [up arrow] SH = t [up arrow] SH. We also have, again from (a) and (b), [for all]j [member of] [1 : K] - {i}, u [up arrow] j = t [up arrow] j. Finally, u [up arrow] i = F.finish = t [up arrow] i. Hence, by definition of a global state, we conclude u = t. Since [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII], we conclude [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII].

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] implies [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]. Let [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] be an arbitrary [P.sub.i]-transition in [R.sup.1]. Hence, by the [P.sub.i]-family definition (2.2), there is some [P.sub.i]-family F in M such that [T.sub.i] [member of] F. By Proposition 4.4.2.2, F is either guarded and nonwriting or unguarded and single-writing. Thus there are two cases.

Case 1: F is unguarded and single-writing. By Definition 3.4.1, there must be a single-writing arc A[R.sub.i] = (s [up arrow] i, true [right arrow] A, t [up arrow] i) in P. Thus, by the global-state transition diagram definition (2.2.2), [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] for some state u such that u [up arrow] i = t [up arrow] i. (End of case 1.)

Case 2: F is guarded and nonwriting. By Definition 3.4.1, there must be a nonwriting arc A[R.sub.i] = (s [up arrow] i, B [right arrow] skip, t [up arrow] i) in P. Now B, the guard of A[R.sub.i], is, by Definition 3.4.1 and Definition 3.3.3, [V.sub.k[member of][1:n]] [b.sub.k], where F = [U.sub.k[member of][1:n]] [F.sub.k], and conditions (G1), (G2) of Definition 3.3.3 are satisfied. Now since [T.sub.i] [member of] F, we have [T.sub.i] [member of] [F.sub.l] for some l [member of] [1 : n]. Since, by assumption, s is reachable in M, we can instantiate (G1) for [T.sub.i] to obtain (since s = T.begin)

s([b.sub.l]) = true.

Therefore, s(B) = true, since [b.sub.l] is a disjunct of B. Hence, by the global-state transition diagram definition (2.2.2), [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII], for some state u such that u [up arrow] i = t [up arrow] i. (End of case 2.)

Thus in both cases, [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] for some state u such that u [up arrow] i = t [up arrow] i. By the global-state transition diagram definition (2.2.2), we have

(c) <s [up arrow] SH> A <u [up arrow] SH> and [for all]j [member of] [1 : K] - {i}, s [up arrow] j = u [up arrow] j.

Also in both cases, [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] by assumption. By the assumption on Kripke structures in Section 2.3, we have

(d) <s [up arrow] SH> A <t [up arrow] SH> and [for all]j [member of] [1 : K] - {i}, s [up arrow] j = t [up arrow] j.

Since A is either skip or a deterministic multiple assignment, we have, from the Hoare triples in (c) and (d), u [up arrow] SH = t [up arrow] SH. We also have, again from (c) and (d), [for all]j [member of] [1 : K] - (i}, u [up arrow] j = t [up arrow] j. Hence, by u [up arrow] i = t [up arrow] i and the definition of a global state, we conclude u = t. Since [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII], we conclude [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII].

PROOF OF PROPOSITION 3.4.4. First, we establish P1, P2 and P3:

(P1) If [pi] is a finite initialized path in [M.sup.1], then [pi] is also a finite initialized path in [M.sup.2].

PROOF OF P1. The proof is by induction on [absolute value of [pi]], the length of [pi]. For the base case, [absolute value of [pi]] = 0, and so [pi] = [s.sup.0], where [s.sup.0] is some state in [S.sup.0]. Since [s.sup.0] is reachable in [M.sup.2] = ([S0.sup.], S, [R.sup.2]) by definition, [pi] is a finite initialized path in [M.sup.2] in this case. For the induction step, we assume the induction hypothesis for [pi] a finite path from some state [s.sup.0] in [S.sub.0] to some state t, and establish P1 for [pi]' consisting of [pi] extended with an arbitrary transition [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]. Since t lies on a finite initialized path in [M.sup.2] (by the induction hypothesis), we have that t is reachable in both [M.sup.1], [M.sup.2]. Hence we can apply Lemma 3.4.3 to conclude [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]. Since [pi] is a finite initialized path in [M.sup.2] (by the induction hypothesis), and [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII], we have that [pi]' is a finite initialized path in [M.sup.2], which concludes the induction step.

(P2) If [pi] is a finite initialized path in [M.sup.2], then [pi] is also a finite initialized path in [M.sup.1].

PROOF OF P2. The proof is exactly symmetric to the proof of P1 above, with the roles of [M.sup.1] and [M.sup.2] interchanged.

(P3) s is a reachable state of [M.sup.1] iff s is a reachable state of [M.sup.2].

PROOF OF P3. The proof is by double implication. For the left-to-right direction, let s be an arbitrary reachable state of [M.sup.1]. Thus, by definition, there is a finite initialized path [pi] in [M.sup.1] which ends in s. By P1 above, [pi] is a finite initialized path in [M.sup.2]. Thus, by definition, s is a reachable state of [M.sup.2]. The right-to-left direction is proven in the same way, with the roles of [M.sup.1] and [M.sup.2] interchanged, and P2 being invoked instead of P1.

From P3, we see that [M.sup.1] and [M.sup.2] have the same reachable states. Thus, from Lemma 3.4.3, [M.sup.1] and [M.sup.2] have the same reachable transitions. Since, by CTL semantics, [M.sup.1], [S.sub.0] [satisfies] f and [M.sup.2], [S.sub.0] [satisfies] f depend only on the reachable portions of [M.sup.1] and [M.sup.2] respectively, the proposition follows.

PROOF OF PROPOSITION 4.4.2.1. Let f be an arbitrary conjunct of the specification. By Section 2.4, f has one of the forms given in the statement of the proposition. Thus there are five cases:

Case 1: f is of the form h, where h [member of] LO(AP), [logical not], [conjunction]). Let s be an arbitrary state of [S"'.sub.0]. By construction of Phase 4, [S"'.sub.0] [subset or equal to] [S'.sub.0]. Hence s [member of] [S'.sub.0]. Thus, by the definition of [S'.sub.0] (Section 4.1.2), there is some state s' [member of] [S.sub.0] such that s is propositionally equivalent to s'. By the soundness of the Emerson and Clarke [1982] synthesis method, M, [S.sub.0] [satisfies] h, and so s' [satisfies] h. (If M = ([S.sub.0], S, R) is given directly, then we assume that all initial states of M satisfy h. In other words, all initial states that violate the initial state specification h are a priori removed from [S.sub.0]. In particular, if h is derived from M as shown in Figure 4, then all initial states of M will satisfy h by construction.) Hence s [satisfies] h, since h is purely propositional. Since s is an arbitrarily chosen state of [S"'.sub.0], we have M"', [S"'.sub.0] [satisfies] h by CTL semantics.

Case 2: f is of the form AGh, where h [member of] LO(AP, [logical not], [conjunction]). Let s be an arbitrary reachable state of M" such that s [not satisfies] h. Since AGh is a conjunct of the specification, h will be added to label(s) in Phase 4 (by construction of Phase 4--see Figure 5).

Hence s will be deleted or made unreachable in Phase 4 (by construction of Phase 4, in particular, the Prop-rule--see Figure 7). Thus, every reachable state of M"' satisfies h. Hence M"', [S"'.sub.0] [satisfies] AGh by CTL semantics.

Case 3: f is of the form AG(p [??] A[q [union] r]), where p, q, r [member of] LO(AP, [logical not], [conjunction]). Let s be an arbitrary reachable state of M" such that s [satisfies] p [conjunction] [logical not] A[q [union] r]. Since AG(p [??] A[q [union] r]) is a conjunct of the specification, A[q [union] r] will be added to label(s) in Phase 4 (by construction of Phase 4--see Figure 5). Hence, in Phase 4, by application of the AU-rule (Figure 7), every fullpath [pi] starting in s such that [pi] [not satisfies] [qUr] will have one of its transitions deleted, and so M"' will not contain fullpath [pi]. When Phase 4 has terminated, every fullpath starting in s (if any) will satisfy [qUr]. If there are no fullpaths starting in s, then s will be made unreachable in M"' (or will be deleted) by repeated applications of the EX-rule (Figure 7), since every path from s terminates in a state with no successors. Hence we conclude that every reachable state in M"' which satisfies p also satisfies A[qUr]. Thus M"', [S"'.sub.0] [satisfies] AG(p [??] A[qUr]) by CTL semantics.

Case 4: f is of the form AG([p.sub.i] [??] E[X.sub.i][q.sub.i]), where [p.sub.i], [q.sub.i] [member of] LO(A[P.sub.i], [logical not], [conjunction]). Let s be an arbitrary reachable state of M" such that s [satisfies] [p.sub.i] [conjunction] [logical not] E[X.sub.i]([p.sub.i] [disjunction] [q.sub.i]). Since AG([p.sub.i] [??] E[X.sub.i][q.sub.i]) is a conjunct of the specification, E[X.sub.i]([p.sub.i] [disjunction] [q.sub.i]) will be added to label(s) in Phase 4 (by construction of Phase 4--see Figure 5). Hence, by application of the E[X.sub.i]-rule (Figure 7), s will be deleted or made unreachable in Phase 4. Hence we conclude that every reachable state in M"' which satisfies [p.sub.i] also satisfies E[X.sub.i]([p.sub.i] [disjunction] [q.sub.i]). Thus M"',[S"'.sub.0] [satisfies] AG([p.sub.i] [??] E[X.sub.i]([p.sub.i] [disjunction] [q.sub.i])) by CTL semantics.

Case 5: f is of the form AG([p.sub.i] [??] A[Y.sub.i][q.sub.i]), where [p.sub.i], [q.sub.i] [member of] LO(A[P.sub.i], [logical not], [conjunction]). By the soundness of the Emerson and Clarke [1982] synthesis method, M, [S.sub.0] [satisfies] AG([p.sub.i] [??] A[Y.sub.i][q.sub.i]), since f is a conjunct of the specification, and M is produced by applying the Emerson and Clarke [1982] synthesis method to the specification. By Proposition 4.1.2.1, M and M' satisfy the same CTL formulae. Hence M', [S'.sub.0] [satisfies] AG([p.sub.i] [??] A[Y.sub.i][q.sub.i]). Also, since M is in reachable form and M, M' are bisimilar (see the proof of Proposition 4.1.2.1), we conclude that M' is in reachable form.

It is easy to see that a global state s satisfies [p.sub.i], [q.sub.i] iff its [P.sub.i]-projection s [up arrow] i satisfies [p.sub.i], [q.sub.i] respectively (since satisfaction of [p.sub.i], [q.sub.i] depends only on the values assigned to atomic propositions in A[P.sub.i], and s, s [up arrow] i agree, by definition, on these values). Now P = [P.sub.1][parallel] ... [parallel][P.sub.K] is extracted from M', and so, by the program extraction definition (2.3), every i-state [s.sub.i] of [P.sub.i] which satisfies [p.sub.i] has as local successors in [P.sub.i] i-states [t.sub.i] which satisfy [q.sub.i.]. In Phase 2, an arc ([s.sub.i], B [right arrow] [//.sub.m [member of] [1:n]] [A.sup.m], [t.sub.i]) of [P.sub.i] is decomposed into arcs having the forms ([s.sub.i], B [right arrow] skip, [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]), ([MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]), [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII], [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]), ..., ([MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII], [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII], [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]), ..., ([MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII], [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII], [t.sub.i]). From the construction of Phase 2, (in particular, the way the local atomic proposition valuations of the "new" states [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] are chosen) we see that each [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII], k [member of] [0 : n-1], satisfies either [p.sub.i] or [q.sub.i]. Since [t.sub.i] satisfies [q.sub.i], and [s.sub.i] is chosen arbitrarily, we have that every i-state in [P".sub.i] which satisfies [p.sub.i] (namely, [s.sub.i] and possibly some of the [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]) has as local successors in [P".sub.i] i-states which either satisfy [P.sub.i] or satisfy [q.sub.i] (the i-states satisfying [q.sub.i] being [t.sub.i] and possibly some of the [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]).

Now M" is the global-state transition diagram of P" = [P".sub.1][parallel] ... [parallel] [P".sub.K]. Thus, by the global-state transition diagram definition (2.2.2) and CTL semantics, M", [S'.sub.0] [satisfies] AG([p.sub.i] [??] A[Y.sub.i]([p.sub.i] [disjunction] [q.sub.i])). We can easily see, by CTL semantics, that removing transitions from M" cannot cause AG([p.sub.i] [??] A[Y.sub.i]([p.sub.i] [disjunction] [q.sub.i])) to be violated. This is because A[Y.sub.i] is the weak nexttime operator. It does not actually require the existence of any transitions per se, but only requires that those transitions that leave a state satisfying [p.sub.i] enter a state satisfying [p.sub.i] [disjunction] [q.sub.i]. Since [S"'.sub.0] [subset or equal to] [S'.sub.0] and R"' [subset or equal to] R" (by construction of Phase 4), we conclude M"',[S"'.sub.0] [satisfies] AG([p.sub.i] [??] A[Y.sub.i]([p.sub.i] [disjunction] [q.sub.i])). []

B. GLOSSARY OF SYMBOLS
[satisfies]                          Satisfies relation of CTL

{}                                   State to formula operator

[up arrow] i                         State projection onto process i

[down arrow] i                       State projection onto all shared
                                     variables and
                                     all processes except i

[M.sup.1], [M.sup.2]                 Kripke structure

M, M', M", M"', [M.sup.iv]           The specific Kripke structures
                                     involved in the synthesis method

P, P', P", P"'                       The specific concurrent programs
                                     involved in the
                                     synthesis method

R, [R.sup.1], [R.sup.2], R", R"',    Transition relation
[R.sup.iv]

S                                    Set of global states

[S.sub.0], [S'.sub.0], [S"'.sub.0]   Set of initial global states

AP                                   The set of atomic propositions

A[P.sub.i]                           The set of atomic propositions of
                                     process i

LO                                   Constructor of sets of
                                     propositional formulae

SH                                   The set of shared variables


ACKNOWLEDGMENTS

We thank Amir Pnueli for suggesting the possibility of synthesizing Peterson's mutual exclusion algorithm, and Anish Arora for suggesting the barrier synchronization example.

(1) We use [1 : K] for the set of natural numbers 1 through K inclusive.

(2) // is the simultaneous parallel assignment operator. Execution of [//.sub.m[member of][1:n] [x.sup.m] := [c.sup.m] is achieved by executing all of the assignments [x.sup.m] := [c.sup.m] simultaneously. Here [x.sup.m] is a shared variable in P, and [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]. Note that the possibility of interference does not arise, since the [c.sup.m] are all constants. If n = 0, then the multiple assignment [//.sub.m[member of][1:n] [x.sup.m] := [c.sup.m] is written as skip.

(3) Alternatively, we can consider s [up arrow] SH as a set of variable bindings {< [x.sub.1], [v.sub.1] >, ..., < [x.sub.m], [v.sub.m] >}. Global state s is then the tuple ([s.sub.1], ..., [s.sub.K], < [x.sub.1], [v.sub.1] > , ..., < [x.sub.m], [v.sub.m] >). This viewpoint is useful later in the description of the synthesis method.

(4) s(B) is defined by the usual inductive scheme: s("x = c") = true iff s(x) = c, s(B1 [conjunction] B2) = true iff s(B1) = true and s(B2) = true, s([logical not] B1) = true iff s(B1) = false.

(5) Termination is obvious, since the right-hand side of A is a list of constants.

(6) We denote various sets of propositional formulae by LO followed by a list of the atomic propositions and boolean operators that can be used in constructing the formulae.

(7) While this paper is self-contained, the reader is referred to Emerson and Clarke [1982] for more detail.

(8) We assume that every process [P.sub.i] contains, between any pair of local states, at most one arc labeled with a given assignment statement. If process [P.sub.i] contains two such arcs, say ([s.sub.i], B1 [right arrow] A, [t.sub.i]) and ([s.sub.i], B2 [right arrow] A, [t.sub.i]), then these can be combined into the single arc ([s.sub.i], (B1 [disjunction] B2) [right arrow] A, [t.sub.i]).

(9) Equivalence is with respect to the Kripke structure M. In other words, F.guard and B agree on every reachable global state u in M whose projection onto [P.sub.i] is F.start, the local start state for a transition in F. That is, M, [S.sup.r] [satisfies] {F.start} [??] (B [equivalent to] F.guard), where [S.sup.r] is the set of reachable states of M. Another way of stating this is [{F.start}.sup.M] [intersection] [F.guard.sup.M] = [{F.start}.sup.M] [intersection] [B.sup.M], where [f.sup.M] = {s | s [satisfies] f and s is a reachable state of M}.

(10) Note that we are not claiming that programs in our model do not use "busy waiting." Busy waiting, however, comes into the picture when we implement the synchronization skeleton model. In an implementation, busy waiting would usually be needed in order to repeatedly test the guard of an arc, so that the arc can be executed when the guard evaluates to true.

(11) In fact F.guard would be replaced by true in the guard simplification step of (Phase 1 of) the synthesis method. See Section 4.1.4.

(12) Equivalence is with respect to the Kripke structure M--see footnote 9.

(13) If we wish to take fault tolerance or self-stabilization [Arora 1992; Arora et al. 1998] properties into account, then the unreachable portions do have to be considered. Since we do not consider such properties in this paper, we ignore "unreachable behavior."

(14) Note the abuse of notation here. Technically, s [up arrow] SH is a mapping; it relates each x [member of] SH to exactly one value in [D.sub.x]. However, in the middle of applying the rules, s [up arrow] SH could relate some x [member of] SH to more than one value in [D.sub.x]. The split-state rule ensures that upon termination s [up arrow] SH is a mapping, for all states s in M. We use the notation < x, c > to denote a variable to value binding here. We say that state s contains the binding < x, c > iff < x, c > [member of] s [up arrow] SH.

(15) Two states are propositionally equivalent iff they agree on all atomic propositions.

(16) An incoming transition is consistent with x = [c.sup.l] iff either (1) it is labeled with x := [c.sup.l], or (2) it is not labeled with an assignment (or equivalently, it is labeled with skip), and it originates in a state containing the binding < x, [c.sup.l] >.

(17) [S'.sub.0] is the set of initial states of the structure M' derived in Phase 1. See Section 4.1.2.

(19) If [V.sub.k[member of][1:n]] [b.sub.k] is false, then all of the [b.sub.k], k [member of] [1 : n] are false. Hence eval([b.sub.k]) returns false for all k [member of] [1 : n].

REFERENCES

ANUCHITANUKUL, A. AND MANNA, Z. 1994. Realizability and synthesis of reactive modules. In Proceedings of the 6th International Conference on Computer Aided Verification. Lecture Notes in Computer Science, vol. 818. Springer-Verlag, Berlin, 156-169.

ARORA, A. 1992. A foundation of fault-tolerant computing. Ph.D. thesis, Department of Computer Sciences, The University of Texas at Austin.

ARORA, A., ATTIE, P. C., AND EMERSON, E. A. 1998. Synthesis of fault-tolerant concurrent systems. In Seventeenth Annual ACM Symposium on Principles of Distributed Computing. ACM Press, 1515 Broadway, New York, NY 10036, 173 - 182.

ATTIE, P. C. 1995. Formal methods for the synthesis of concurrent programs from temporal logic specifications. Ph.D. thesis, Dept. of Computer Sciences, The Univ. of Texas at Austin.

ATTIE, P. C. 1999. Synthesis of large concurrent programs via pairwise composition. In CONCUR'99: 10th International Conference on Concurrency Theory. Lecture Notes in Computer Science 1664. Springer-Verlag, Heidelberg, Germany.

ATTIE, P. C. AND EMERSON, E. A. 1998. Synthesis of concurrent systems with many similar processes. ACM Trans. Program. Lang. Syst. 20, 1 (Jan.), 51-115. Preliminary version appears in Sixteenth ACM Symposium on Principles of Programming Languages, 1989.

BACK, R. 1989. Refinement calculus, part ii: parallel and reactive programs. In Stepwise refinement of distributed systems, J. de Bakker, W. de Roever, and G. Rozenberg, Eds. Lecture Notes in Computer Science 430. Springer-Verlag, Heidelberg, Germany, 67-93.

BACK, R. AND VON WRIGHT, J. 1994. Trace refinement of action systems. In CONCUR'94:Concurrency theory, B. Johnsson and J. Parrow, Eds. Lecture Notes in Computer Science 836. Springer-Verlag, Heidelberg, Germany, 367-384.

BROWNE, M., CLARKE, E. M., AND GRUMBERG, 0. 1988. Characterizing finite kripke structures in propositional temporal logic. Theoretical Computer Science 59, 115-131.

CHANDY, K. M. AND MISRA, J. 1988. Parallel Program Design. Addison-Wesley, Reading, Mass.

CLARKE, E. M., GRUMBERG, O., AND BROWNE, M. C. 1986. Reasoning about networks with many identical finite-state processes. In Proceedings of the 5th Annual ACM Symposium on Principles of Distributed Computing. ACM, New York, 240 - 248.

DIJKSTRA, E. W. 1976. A Discipline of Programming. Prentice-Hall Inc., Englewood Cliffs, N.J.

DILL, D. AND WONG-TOI, H. 1990. Synthesizing processes and schedulers from temporal specifications. In International Conference on Computer-Aided Verification. Number 531 in LNCS. Springer-Verlag, Heidelberg, Germany, 272-281.

EMERSON, E. A. 1990. Temporal and modal logic. In Handbook of Theoretical Computer Science, J. V. Leeuwen, Ed. Vol. B, Formal Models and Semantics. The MIT Press/Elsevier, Cambridge, Mass.

EMERSON, E. A. AND CLARKE, E. M. 1982. Using branching time temporal logic to synthesize synchronization skeletons. Sci. Comput. Program. 2, 241 - 266.

FRANCEZ, N. 1986. Fairness. Springer-Verlag, New York.

GRIBOMONT, E. 1990. Stepwise refinement and concurrency: the finite-state case. Sci. Comput. Program. 14, 2-3 (Oct.), 185-228.

GRIBOMONT, E. 1993. Concurrency without toil: a systematic method for paralel program design. Sci. Comput. Program. 21, 1 (Aug.), 1-56.

HERLIHY, M. 1991. Wait-free synchronization. ACM Trans. Program. Lang. Syst. 11, 1 (Jan.), 124-149.

HOARE, C. A. R. 1969. An axiomatic basis for computer programming. Commun. ACM 12, 10, 576-580, 583.

LAMPORT, L. 1990. A theorem on atomicity in distributed algorithms. Distributed Computing 4, 2, 59-68.

LYNCH, N. AND TUTTLE, M. 1987. Hierarchical correctness proofs for distributed algorithms. In Proceedings of the 6'th Annual ACM Symposium on Principles of Distributed Computing. ACM Press, 1515 Broadway, New York, NY 10036, 137 - 151.

LYNCH, N. AND VAANDRAGER, F. 1995. Forward and backward simulations -- part I: Untimed systems. Inform. and Comput. 121, 2 (Sept.), 214-233.

MANNA, Z. AND PNUELI, A. 1995. Temporal verification of reactive systems: safety. Springer-verlag, New York.

MANNA, Z. AND WOLPER, P. 1984. Synthesis of communicating processes from temporal logic specifications. ACM Trans. Program. Lang. Syst. 6, 1 (Jan.), 68-93. Also appears in Proceedings of the Workshop on Logics of Programs, Yorktown-Heights, N.Y., Springer-Verlag Lecture Notes in Computer Science (1981).

PETERSON, G. 1981. Myths about the mutual exclusion problem. IPL 12, 3 (June), 115-116.

PNUELI, A. AND ROSNER, R. 1989a. On the synthesis of a reactive module. In Proceedings of the 16th ACM Symposium on Principles of Programming Languages. ACM, New York, 179-190.

PNUELI, A. AND ROSNER, R. 1989b. On the synthesis of asynchronous reactive modules. In Proceedings of the 16th ICALP. Lecture Notes in Computer Science, vol. 372. Springer-Verlag, Berlin, 652-671.

SINGH, A., ANDERSON, J., AND GOUDA, M. 1994. The elusive atomic register. J. ACM 41, 2 (Mar.), 311-339.

Received July 1998; accepted June 1999

An extended abstract containing some of these results was presented at the ACM Symposium on Principles of Distributed Computing, Philadelphia, Pennsylvania, 1996, under the title "Synthesis of Concurrent Systems for an Atomic Read / Atomic Write Model of Computation." P.C. Attie was supported in part by the National Science Foundation under CAREER grant number CCR-0096356. E. A. Emerson was supported in part by NSF Grants CCR-9804736 and CCR-0098141 together with Texas ARP project 003658-0650-1999.

Authors' addresses: P.C. Attie, College of Computer Science, Northeastern University, Boston, MA 02115; E.A. Emerson, Department of Computer Sciences, The University of Texas at Austin, Austin, TX 78712.
COPYRIGHT 2001 Association for Computing Machinery, Inc.
No portion of this article can be reproduced without the express written permission from the copyright holder.
Copyright 2001 Gale, Cengage Learning. All rights reserved.

Article Details
Printer friendly Cite/link Email Feedback
Author:Attie, Paul C.; Emerson, E. Allen
Publication:ACM Transactions on Programming Languages & Systems
Geographic Code:1USA
Date:Mar 1, 2001
Words:30121
Previous Article:A schema for interprocedural modification side-effect analysis with pointer aliasing.
Next Article:Type elaboration and subtype completion for Java bytecode.
Topics:

Terms of use | Privacy policy | Copyright © 2019 Farlex, Inc. | Feedback | For webmasters