Outline for January 11, 2001 1. Greetings and felicitations! a. First part of project due Friday b. Web page up and running! 2. Process models a. Theorem: If a system is mutually noninterfering, it is determinate. b. Theorem: Let fp be an interpretation of process p. Let be a system of processes, with p ? . If for all such p, domain(p) Ř and range(p) Ř, but fp unspecified, is determinate for all fp, then all processes in are mutually noninterfering c. Maximally parallel system: determinate system for which the removal of any pair from the relation Ć makes the two processes in the pair interfering processes. 3. Critical section problem a. Mutual exclusion b. Progress c. Bounded wait 4. Classical problems a. Producer/consumer b. Readers/writers (first: readers priority; second: writers priority) c. Dining philosophers 5. Basic language constructs a. Semaphores b. Send/receive 6. Evaluating higher-level language constructs a. Modularity b. Constraints c. Expressive power d. Ease of use e. Portability f. Relationship with proram structure g. Process failures, unanticipated faults (exception handling) h. Real-time systems 7. Higher-level language constructs a. Monitors b. Crowd monitors c. Invariant expressions d. CSP e. RPC f. ADA? Mutual Non-Interference and Determinism Introduction A determinate system of processes is a set of process that always produces the same output given the same input. A mutually non-interfering set of processes is a set of processes that do not interfere with the input or output of one another. The question is, to what degree are these the same concepts? Formal Definitions and Notations ˇ A system of processes S = (, Ć) is a set of processes = { p1, -, pn } and a precedence relation Ć: Ľ. The Ć relation is a partial ordering (we define p Ć p as true). When p Ć q, process p must complete before pro- cess q may begin. ˇ Each process p ? has an associated set of input memory locations called domain(p) and an associated set of output memory locations range(p) . An interpretation fp of p associates values with each set of memory loca- tions. The set of all inputs to S is abbreviated domain(S), and the set of all outputs from S is abbreviated range(S). ˇ Two systems of processes S = (, Ć) and S' = (', Ć') are equivalent if a. = '; b. Ć Ć'; and c. if S and S' are given the same element of domain(S), then they output the same element of range(S). ˇ An execution sequence a is any string of process initiation and termination events satisfying the precedence con- straints of the system. ˇ V(Mi, a) is the sequence of values written into memory location Mi at the termination of processes in a. The final value stored in Mi after execution sequence a completes is represented by F(Mi, a). ˇ A determinate system of processes is a system of processes S for which each element of domain(S) produces the same set range(S) regardless of the order or overlapping of the elements of S. More formally, a system S is deter- minate if, for any initial state and for all execution sequences a and a' of S, V(Mi, a) = V(Mi, a') ˇ A mutually noninterfering system of processes is a system of processes S in which all pairs of processes meet the Bernstein conditions. Processes p and q are noninterfering if either process is a predecessor of the other, or the processes satisfy the Bernstein conditions. ˇ The initiation of a process p is writtten p, and the termination of p is written p. Relationship of Determinate Systems and Mutually Noninterfering Systems Theorem 1: If a system is mutually non-interfering, it is determinate. Theorem 2: Let S be a system with domain(p) and range(p) specified, range(p) , for all p ? , and fp unspeci- fied. Then if S is determinate for all fp, it is mutually non-interfering. Proofs The following lemma is helpful: Lemma: Let S be a mutually noninterfering system. Let p be a terminal process of S. If a = bpgpd is an execution sequence of S, then a' = bgdpp is an execution sequence of S for which V(Mi, a) = V(Mi, a') for all i. Proof: As p is a terminal process in S, it has no successors in S. Hence a' satisfies the precedence constraints of S. So a' is an execution sequence. We now consider two cases. 1. Mi ? range(p). Note p does not write memory locations not in range(p). Consider any process p' with p' in d. As p and p' are mutually noninterfering, range(p) Ť domain(p') = . So all such p' find the same values in domain(p') whether the execution sequence is a or a'. Thus, V(Mi, a) = V(Mi, a'). 2. Mi ? range(p). Let p' in gd. As p and p' are mutually noninterfering, domain(p) Ť range(p') = . So no p' in gd writes into an element of domain(p). Hence for all Mj ? domain(p), V(Mj, b) = V(Mj, bgd). By definition, for all Mj ? domain(p), F(Mj, b) = F(Mj, bgd). As p has the same input for both a and a', it writes the same value into each Mi ? range(p) in a and a'. Let v denote the value that p writes into Mi in a. Then V(Mi, a) = V(Mi, bpgpd) as no process p' in d writes into an element of range(p) = (V(Mi, bpg), v) as p writes v into Mi = (V(Mi, b), v) as no process p' in g writes into an element of range(p) = (V(Mi, bgd), v) as no process p' in g writes into an element of range(p) = V(Mi, bgdpp) as p writes v into Mi = V(Mi, a') This proves the lemma. n Proof of Theorem 1: We proceed by induction on the number k of processes in a system. Basis: k = 1. The claim is trivially true. Hypothesis: For k = 1, -, n-1, if a system of k processes is mutually noninterfering, it is determinate. Step: Let S be an n process system of mutually noninterfering processes. If S has exactly one execution sequence, it is determinate. So, assume that S has two distinct execution sequences a and b. Let p be a terminal process of S, and form a' and b' according to the lemma. Then a' = a''pp V(Mi, a) = V(Mi, a') for all i such that 1 i m b' = b''pp V(Mi, b) = V(Mi, b') for all i such that 1 i m Now form the n-1 process system S' = ( - { p }, Ć'), where Ć' is formed by deleting from Ć all pairs with p in them. Clearly, a'' and b'' are execution sequences of S'. Further, by the induction hypothesis, V(Mi, a'') = V(Mi, b'') for all i such that 1 i m. This means that the values in the elements of domain(p) are the same in both a'' and b''; in other words, F(Mj, a'') = F(Mj, b'') for all Mj ? domain(p). As the inputs for p are the same in both execution sequences, the outputs will also be the same. It follows that p writes the same value v into Mi ? range(p) in both a' and b'. Hence for Mi ? range(p): V(Mi, a) = V(Mi, a') by the lemma = V(Mi, a'') as Mi ? range(p) = V(Mi, b'') by the induction hypothesis = V(Mi, b') as Mi ? range(p) = V(Mi, b) by the lemma and for Mi ? range(p): V(Mi, a) = V(Mi, a') by the lemma = (V(Mi, a''), v) p writes v into Mi = (V(Mi, b''), v) by the induction hypothesis = (V(Mi, b'), v) p writes v into Mi = V(Mi, b) by the lemma Either way, V(Mi, a) = V(Mi, b). Hence S is determinate, completing the induction step and the proof. n Proof of Theorem 2: We prove this theorem by contradiction. Let S be a determinate system. Let p, p' ? be inter- fering processes. Then there exist execution sequences a = bppp'p'g a' = bp'p'ppg Consider the Bernstein conditions. As p and p' are interfering, at least one of those conditions does not hold. We examine them separately. 1. Let Mi ? range(p) Ť range(p'). We choose the interpretation fp so that p writes the value u into Mi, and we choose the interpretation fp' so that p' writes the value v into Mi, and u v. But then V(Mi, bppp'p') = (V(Mi, b), u, v) and V(Mi, bp'p'pp) = (V(Mi, b), v, u). This means S is not determinate, contradicting hypothesis. So range(p) Ť range(p') = . 2. Let Mi ? domain(p) Ť range(p'). As range(p) , take Mi ? range(p). Choose the interpretation fp' so that p reads different values in a and a'; that is, F(Mj, b) F(Mj, bp'p') for some j such that 1 j m. Also, choose fp so that p writes u in a and v in a', where u v. But then V(Mi, bppp'p') = V(Mi, bpp) as range(p) Ť range(p') = Ř = (V(Mi, b), u) V(Mi, bp'p'pp) = (V(Mi, bp'p'), v) = (V(Mi, b), v) as range(p) Ť range(p') = Ř As u v, this means that S is not determinate, contradicting hypothesis. So domain(p) Ť range(p') = . [As an aside, if range(p) = , then Mi ? range(p) and p and p' are noninterfering. Hence there is no contradiction.] 3. By symmetry, the argument for case 2 also shows that range(p) Ť domain(p') = . In all three cases, the Bernstein conditions must hold. This completes the proof. n