Synopsis -------- It's been a while since I've sent out a TLA message. Time to wake everyone up. Just two things to report. They are summarized here and discussed in detail below. 1. Many people believe that you can simplify reasoning about a closed system by breaking into the composition of simpler open systems and reasoning independently about the open components. (Or that you can simplify reasoning about an open system by decomposing it into simpler open components.) That's wrong. Going from closed to open systems always means more work. 2. Martin Abadi and I have written basically two papers on specification: "The Existence of Refinement Mappings" (SRC Report 29, to appear in Theoretical Computer Science in a couple of months) and "Composing Specifications" (SRC Report 66, presented at a REX Workshop in the Netherlands in 1989). These were purely semantic--talking about sets of sequences, not logic. There are two basic semantic concepts: closed sets (also known as safety properties) and realizability. We have recently realized that these semantic concepts are expressible within TLA. More precisely, the "closure" and "realizable-part-of" operators, which were defined semantically, can be defined in TLA. An amusing question is whether all the theorems we proved semantically can be proved within TLA. This might make a nice PhD thesis topic (hint, hint, to all of you in academia). The first topic reads easily enough in ASCII, so I haven't bothered formatting it for LaTeX. (I also thought it would interest more of you than the second part.) The second topic is formatted using the spec92 style file. If you want to read everything together, you can just copy the first part of the file into the second, after the begin{spec} command. Opening Closed Systems ---------------------- I will describe the argument in terms of TLA, where the specification of an open system is a formula E => M, where E is the environment assumption and M the system guarantee, and parallel composition is conjunction. The argument holds for any rely/guarantee style of specification. Just replace E => M by (E,M) or any other syntax you like, and replace /\ by || or however you want to represent parallel composition. Suppose you want to prove a property P about a system S with specification E => M. What you want to prove is that the property P holds when the system is combined with a correct environment--one that satisfies the system's environment assumption. In other words, you have to prove: (1) E /\ M => P Now, suppose it were possible to simplify the task by decomposing the system into two subsystems S1 and S2. Presumably the reason this will simplify things is that property P is actuallly guaranteed by one of the subsystems, say S1. So, you want to prove that S satisfies P by decomposing S into the composition of S1 and S2 and proving S1 satisfies P. Proving S1 satisfies P means proving (2) E1 /\ M1 => P. Decomposing S into S1 and S2 means finding E1, M1 and E2, M2 so that the specification of S1 is (E1 => M1) and the specification of S2 is (E2 => M2). Moreover, the guarantees M1 and M2 of the subsystems aren't going to be random; for S1 and S2 to be a decomposition of S, their combined guarantees must be the same as S's. In other words, (3) M1 /\ M2 = M But what do you have to prove to show that S1 and S2 compose properly? In other words, what must be true for their composition to satisfy the specification E => M1 /\ M2, which asserts that, when placed in an environment satisfying E, it guarantees M1 and M2? For S1 and S2 to compose properly, the environment assumptions of each have to be satisfied in the composition. In other words, when S1 is run in an environment consisting of S2 and an environment satisfying E, then E1 is satisfied. Since M2 is the guarantee provided by S2, the obvious condition is (4) E /\ M2 => E1 This is actually too strong to be provable in practice, and one really needs a weaker hypothesis that looks something like (5a) E /\ M1 /\ M2 => E1 The reason (4) isn't good enough is that E /\ M2 doesn't say anything about what the first component system is doing, so you can't deduce any invariants from it. The left-hand side of (5a) essentially describes the closed system consisting of S1, S2, and their surrounding environment, so you prove invariants with it. Similarly, to prove that S2's environment assumption is satisfied in the composition, you also have to prove the analogous (5b) E /\ M1 /\ M2 => E2 So, to prove P by decomposing S into S1 and S2, you you have to prove (2), (3), (5a), and (5b). Moreover, (5a) and (5b) are oversimplified. When liveness is involved, they are too weak to yield a valid composition, and they need to be modified (by adding some closure operators and some other conditions on the E's and M's). But even forgetting this additional complication, (2), (3), and (5a), without (5b), imply (1). If you can find the E's and M's to do the decomposition into open systems, then you could have found the formulas E1 and M1 by themselves such that (6) E /\ M => E1 /\ M1 proved (2) and deduced (1) without doing any decomposition. At best, decomposing the system into open subsystems produces a proof that is equivalent to one that you could have done working completely in the closed system. In reality, it's a lot worse. In practice, decomposing M as M1 /\ M2 is straightforward. For example, if S is a two-process system, M1 and M2 will be the specifications of the individual processes. However, E1 and E2 are likely to be much, much, much more complicated than E. For example, consider any mutual exclusion algorithm from the literature--the mutual exclusion literature, not the verification literature! This will essentially be a closed system, so E will equal TRUE (or, if not, will be either simple or irrelevant to mutual exclusion). Imagine trying to state the environment assumption for an individual process i that guarantees that the other process is not in the critical section when process i is. Those E's will be very complicated--much more complicated than the actual invariant used to prove mutual exclusion of the closed system. I maintain that one would have to be crazy to try to prove a mutual exclusion algorithm in such an opened-up fashion. And I will continue to maintain that until someone proves me wrong by giving such a proof for a nontrivial mutual exclusion algorithm (say, my "Fast Mutual Exclusion Algorithm", published not too many years ago in TOCS). One decomposes systems into open subsystems to allow the subsystems to be implemented by different people (or by one person, with limited memory, at different times). Doing the decomposition adds the significant cost of figuring out exactly what assumptions one part of the system makes of the other part in order for the two parts to implement the whole system correctly. This is so hard that, to gain the benefit of separate implementation, one will usually sacrifice efficiency by writing simpler but stronger environment assumptions E1 and E2, and correspondingly stronger module guarantees M1 and M2 to make (5a) and (5b) valid. (Put another way, modularity rules out global optimization that takes advantage of simultaneous knowledge of the implementations of both components.) % LaTeX file begins here. % \documentstyle[11pt,spec92]{article} \renewcommand{\o}{\circ} \newcommand{\C}{\cal C} \subscripts \superscripts \begin{document} % Insert anything else you want printed after the following % \begin{spec} command % \begin{spec} Representing Closure -------------------- The closure :C:(P) of a property P is the smallest safety property containing P. (We used to denote the closure operator by an overbar. But I like using overbar for refinement mapping, so we are probably going to switch to the :C:(...) notation.) A behavior satisfies :C:(P) iff every finite prefix of the behavior can be extended to a behavior in P. Here's the definition of :C:(F) for any TLA formula F. Let v be an n-tuple of variables containing all variables that occur free in F, let w be an n-tuple of variables all distinct from those of v, and let b be a single variable distinct from the variables in v and w. First, define B == (b = 0) /\ [][b' = 1]_b /\ <>(b = 1) Formula B asserts that b equals 0 for a finite time, then equals 1 forever. Letting F(w/v) denote the result of substituting the variables of w for the variables of v, we have :C:(F) == :A: b : B => (:E: w : F(w/v) /\ [](b=0 => v=w)) The formula F(w/v) /\ [](b=0 => v=w) asserts that the w-variables satisfy F, and that the w-variables and the v-variables are equal as long as b is zero. The ":E: w" asserts that there is some way to choose the w-variables so that this is true. Representing the Realizable Part --------------------------------- In the past, we defined the :mu:-realizable part R_[:mu:](P) of a property P using a semantics in which state-changes were labeled and :mu: was a set of labels. We are now going to do things a la TLA, so :mu: is just going to be an action--a :mu:-step is a step that is attributed to the system. A :mu:-step will always change the value of some variable, so there will be no stuttering :mu: steps. The realizable part R_[:mu:](P) is the subset of behaviors that can be obtained by "strategies" that implement P. A strategy is a rule for choosing :mu:-steps. Formally, it is a mapping that assigns to a sequence of states (representing the execution history up to that point) either a state (the next state the system wants to produce) or else the special value :bot: (indicating that the system doesn't want to do anything). In the following, f denotes a rigid variable (a constant), v denotes an n-tuple of variables containing all variables that are in :mu: or in the TLA formula F, and h denotes a variable different from any of the variables of v. First, we define some notation for talking about sequences of n-tuples of values: VAL^n : the set of all n-tuples of values (VAL^n)^* : the set of all finite sequences of elements of VAL^n <<>> : the empty sequence h :o: <> : the sequence obtained by concatenating the element v \\ to the end of the sequence h. |h| : the length of the sequence h . last(h) : the last element of the sequence h. The last three are unspecified unless h is in (VAL^n)^* and v is in VAL^n. Moreover, last(h) is unspecified if h = <<>>. We assume that :bot: is not in VAL^n. Next, we define a formula H essentially asserting that h is a history variable recording the sequence of all past values of v: H == /\ (h = <>) /\ [][h' = h :o: <>]_[(h,v)] /\ :A: n : (n :in: Naturals => <>(|h| > n)) Note that the first two conjuncts imply that h records all changes to v, and may also record some steps in which v didn't change. The third conjunct asserts that h gets arbitrarily long. Hence, if v eventually stutters forever, then this gets recorded in h. Next, we define the formula Strategy(:mu:,f), asserting that f is a :mu:-strategy. A :mu:-strategy must produce only :mu:-steps, so the definition is as follows. Strategy(:mu:,f) == :A: h : (h :in: VAL^n) /\ (|h| # 0) => \/ :mu:(last(h)/v, f(h)/v') \/ f(h) = :bot: Next, Outcome(:mu:,f) is defined to be the set of all outcomes obtained by playing the strategy f against an opponent who can make only ~:mu: moves, and who gives the strategy infinitely many chances to play. Outcome(:mu:,f) == :E: h : /\ H \\\\\ /\ [][:mu: => v'=f(h)]_[(h,v)] \\\\\ /\ []<><:mu:>_[(h,v)] \/ []<>(f(h) = :bot:) The first conjunct asserts that h is keeping history. The second asserts that every :mu: step is done according to strategy f, and the third asserts that either there are infinitely many :mu: steps, or else that infinitely often the strategy was willing to "pass". Finally, the realizable part R_[:mu:](F) of F asserts that the behavior can be produced by some strategy all of whose :mu:-outcomes satisfy F. R_[:mu:](F) == :E: f : /\ :A: v : O_[:mu:](f) => F \\\\\\\\ /\ O_[:mu:](f) Remember that f is a rigid variable--its value doesn't change during the execution. I have a feeling that all the relevant theorems from our two papers involving closure and R_[:mu:] can be proved in TLA using only the rules in the TLA report, plus the rules asserting the validity of adding history and prophecy variables. (See "The Existence of Refinement Mappings".) I also have a feeling that doing so would involve a lot of work. \end{spec} \end{document}