The total correctness of the Peterson's Algorithm has been proved. States and transitions were fixed by the program. Runtime environment considered is interleaving concurrency with shared memory. Invariant of the program was constructed. All reasoning provided in terms of Method for software properties proof in Interleaving Parallel Compositional Languages (IPCL). Conclusions about adequacy of the Method usage for such a kind of tasks (thanks to flexibility of composition-nominative platform) and its practicality as well as ease of use for realworld systems have been made based on this and other author's works.
if b then P1 else P2 | while b do P | x:=e| P1 || P2, where x:=e is an atomic, vector assigning and P1 || P2 implies interleaving parallelism.
Let us define compositional semantics of IPCL. The semantics of the first three compositions is standard while semantics of interleaving parallelism is defined through its arguments semantics and syntactic context in traditional way with its algebraic and semantic properties. An Index-parameter of the semantics function is a syntactic context - piece of the program or the program itself. So:
sem A ; B (d) = d —’ sem A (d) —’ sem B (d —’ sem A (d)) where —’ – component-wise superposition of Cartesian product of nominative data: d1 —’ d2 = (Pr1(d1) — Pr1(d2), Pr2(d1) — Pr2(d2)) Pri(d) is a projection of the Cartesian product d by the i-th component, d1, d2 Œ D¥D,
This small modification is due to the fact that data is considered as two-component one – such that contains
"global" and "local" parts and — – is a simple operation of the data superposition (two nominal or nominative sets) in
accordance with [
Semantics of “:=”: sem x := e (d) = d —’ f (d), where f Œ Oper – is a (semantic) fucntion, which complies with syntactic operator x := e. An assignment (the result of f) provides two-component result, as global and local data are evaluated, and superposition is occurring to the relevant components of d data: global variables – to the first component, local variables – to the second; x and e are the vectors of names and values (expressions) respectively,
semantics of “if”: sem if b then P else Q (d) = sem P (d), iff b(d) = True, sem if b then P else Q (d) = sem Q (d), iff b(d) = False,
semantics of “while”: sem while b do P (d) = sem P ; while b do P (d), iff b(d) = True, sem while b do P (d) = d, iff b(d) = False, semantics of “||”: || is associative and commutative: sem ( A || B ) || C (d) = sem A || ( B || C ) (d) sem A || B (d) = sem B || A (d)
on the syntactic level it means respectively: ((A || B) || C) (d) = (A || ( B || C )) (d) (A || B) (d) = (B || A) (d)
|| relatively to “if”: sem if b then P else Q || R (d) = sem P || R (d), iff b(d) = True, sem if b then P else Q || R (d) = sem Q || R (d), iff b(d) = False, sem if b then P else Q ; P’ || R (d) = sem P ; P’ || R (d), iff b(d) = True, sem if b then P else Q ; P’ || R (d) = sem Q ; P’ || R (d), iff b(d) = False, || relatively to “while”: sem while b do P || R (d) = sem P ; while b do P || R (d), iff b(d) = True, sem while b do P || R (d) = sem R (d), iff b (d) = False, sem while b do P ; P’ || R (d) = sem P ; while b do P ; P’ || R (d), iff b (d) = True, sem while b do P ; P’ || R (d) = sem P’ || R (d), iff b (d) = False,
|| relatively to “;”: sem ( A ; B ) || P (d) = sem A ; ( B || P ) (d), sem A || P (d) = sem A ; P (d), where A, B, C, P, P’, Q, R Œ Terms – programs in IPCL (terms in IPCL Algebra), b is a syntax notation of an appropriate condition of the predicate pred from Pred that is b (d) = sem b (d) = pred (d) and d Œ D¥D.
In all the above definitions if the value of b (d) is undefined then the value of the left side of the relevant equality will also be undefined. Similarly, if any of the definitions of the right side of equality is undefined then the value of the left side is undefined.
F is a set of functions for the data conversion, C is the compositions over functions from F. F=Oper»Pred,
where Oper=D¥D Æ D¥D and Pred=D¥D Æ {True, False}, where the first occurrence of D to the Cartesian product is
“global data” while the second is “local data” for the current process; functions which return values from the set
{True, False} (predicates) do not change the current state (i.e. does not have “side effect”) of data D¥D – they are used
as conditions in branching and cycle operators; D=ND(V,W) in the usual sense (as simple nominative data [
The main idea of the Peterson’s algorithm is to use three variables, flag1, flag2 and turn. flag1 or flag2 value of 1 indicates that the process n wants to enter the critical section. Entrance to the critical section is granted for process T1 if T2 does not want to enter its critical section or if T2 has given priority to T1 by setting turn to 1. Also entrance to the critical section is granted for process T2 if T1 does not want to enter its critical section or if T1 has given priority to T2 by setting turn to 2.
According to the method for program’s properties correctness proof [
[M12] turn∶ = 2; T2≡ [M21] flag2∶ =1; [M22] turn∶ = 1; while [M13] (flag2 = 1 && turn = 2) do skip; [M14] r≔ do_critical_operations(); //critical section [M15] flag1∶ = 0;[M16] while [M23] (flag1 = 1 && turn = 1) do skip; [M24 ] r≔ do_critical_operations(); //critical section [M25] flag2∶ = 0;[M26]
In this work while-cycle condition (for instance in T1 program: ????2 = 1 && ???? = 1) is considered as an atomic operation while we may as well use the method dividing this process into three independent stages, like: ???????2 = ???? 2; ??????? =????; ?ℎ???(???????2 = 1 &&??????? = 1) do begin end; ???????2 =????2; ??????? =????;
??????? =??||??.
The state of this program will be as follows: ????? = (?1,?2,[????1↦ ?1,????2↦ ?2,???? ↦ ?],?1,?2), ??????????? = {?1 →?2 |?1,?2∈ ?????? (??11(?1,?2) ??12(?1,?2) ??13(?1,?2)∨
∨ ∨ ??14(?1,?2) ??15(?1,?2) ??16(?1,?2)∨
∨ ∨ ??21(?1,?2) ??22(?1,?2)∨??23(?1,?2)∨
∨ ??24(?1,?2) ??25(?1,?2)∨??26(?1,?2)},
∨ where ?1 ∈ {? ??, ? ??, ? ??, ? ??, ? ??, ? ??} – labels of T1; ?2 ∈ {? ??, ? ??, ? ??, ? ??, ? ??, ? ??} – labels of T2; [????1 ↦ ?1,????2 ↦ ?2,???? ↦ ?] – global data; d1 and d2 are the local data of T1 and T2 respectively.
∧ where each predicate??ij ?= 1:2, ?= 1:6 describes the possible program step between states.
Tr11(S1,S2) = (Pr1(S∧1)= M11) (Pr1(S2) = M12) ∧(Pr2(S1) = Pr2(S2)) ∧(Pr3(S1) = d) ∧(Pr3(S2) = d ∇[flag1↦1]) ∧ ∧ (Pr4(S1) = Pr4(S2)) (Pr5(S1) = Pr5(S2))
Tr12(S1,S2) = (Pr1(S∧1)= M12) (Pr1(S2) = M13) ∧(Pr2(S1) = Pr2(S2)) ∧(Pr3(S1) = d) ∧(Pr3(S2) = d ∇[turn↦2]) ∧ ∧ (Pr4(S1) = Pr4(S2)) (Pr5(S1) = Pr5(S2))
Tr13(S∧1,S2) = (Pr1(S1) = M13) (Pr1(S2) = M13) (Pr2(S1) = Pr2(S2)) ∧(Pr3(S1) = Pr3(S2) = [flag1↦ f1, flag2↦ f2, turn ∧ ∧ ∧ ∧ ∧ ↦ t]) (Pr4(S1) = Pr4(S2)) (Pr5(S1) = Pr5(S2)) (f2 = 1) (t = 2)
Tr14(S∧1,S2) = (Pr1(S1) = M13) (Pr1(S2) = M14) (Pr2(S1) ∨=t≠P2r2)(S2)) ∧(Pr3(S1) = Pr3(S2) = [flag1↦ f1, flag2↦ f2, turn ∧ ∧ ∧ ∧ ↦ t]) (Pr4(S1) = Pr4(S2)) (Pr5(S1) = Pr5(S2)) (f2 ≠ 1
Tr15(S1,S2) = (Pr1(S1) = M14) (Pr1(S2) = M15) ∧(Pr2(S1) = Pr2(S2)) (Pr3(S1) = Pr3(S2)) ∧(Pr4(S1) = d1) ∧(Pr4(S2) = ∧ ∧ ∧ func1(d1)) (Pr5(S1) = Pr5(S2))
Tr16(S1,S2) = (Pr1(S∧1)= M15) (Pr1(S2) = M16) ∧(Pr2(S1) = Pr2(S2)) ∧(Pr3(S1) = d) ∧(Pr3(S2) = d ∇[flag1↦0]) ∧ ∧ (Pr4(S1) = Pr4(S2)) (Pr5(S1) = Pr5(S2))
Pr1(S) = M11 ∧Pr2(S) = M21} StartStates = {S ∈ States |
Pr1(S) = M16 ∧Pr2(S) = M26} FinalStates = {S ∈ States |
In these terms the mutual exclusion condition for the algorithm, that no two concurrent processes are in their critical section at the same time, can be formulated as: ÿ (Pr1(S) ∈ {M14, M15} ∧Pr2(S) ∈ {M24, M25})
∧ ∧ ∧ Inv(S)= I1(S) I2(S) I3(S) I4(S), where I1(S) = Pr1(S) ∈ {M12, M13, M14, M15} → flag1 ⇒(Pr3(S)) = 1, (Pr2(S) ∉ {M24, M25} ∧ I2(S) = Pr1(S) ∈ {M14, M15} → Pr2(S) = M23 → turn ⇒(Pr3(S)) = 1), I3(S) = Pr2(S) ∈ {M22, M23, M24, M25} → flag2 ⇒(Pr3(S)) = 1, (Pr1(S) ∉ {M14, M15} ∧ I4(S) = Pr2(S) ∈ {M24, M25} → Pr1(S) = M13 → turn ⇒(Pr3(S)) = 2)
The idea of invariant Inv(S) is clear and follows from the definition of critical section. If T1 is located previously to while-cycle {M12, M13} or is inside its critical section {M14, M15}, then flag1 = 1, namely it wants to enter critical section (getting access to the resource). If T1 “goes through” while-cycle {M14, M15}, that means it comes out of the cycle (entrance to critical section and getting access to the resource), then the other process (T2) is outside critical section (i.e. not in {M24, M25}), and also if T2 is located previously to critical section {M23} – then it does not have an access, because it is T1's turn to entrance now: turn = 1.
The proof that invariant holds true over all transitions is rather technical and will not be presented here [
Pr1(S) ∈ {M14, M15} → Pr2(S) ∉ {M24, M25} ∧Pr2(S) ∈ {M24, M25} → Pr1(S) ∉ {M14, M15} which is equal to: ÿ (Pr1(S) ∈ {M14, M15} ∧Pr2(S) ∈ {M24, M25}) namely, the mutual exclusion condition: for any state S it is not possible to appear in critical section (marks M14, M15 for T1 and marks M24, M25 for T2) for both processes (T1 and T2) at the same time.
Let us prove that that the program system ??????? = ??||?? will stop in the shown model.
According to the algorithm structure the only problem space is a cycle. We have to prove that as soon as the process T2 has finished its work (flag2∶ = 0), the process T1 will leave the cycle (we will not observe the infinite cycle).
Proof by contradiction: let us suppose that the process T1 after the label M13 will get into the label M13 which means the true value of the while-cycle condition. According to the transition Tr13(S1,S2) flag2 = 1. From the fact that none of transitions of T1 will influence the global variable flag2 and from the condition that the process T2 has finished and thus due to Tr16(S1,S2), we have that flag2 = 0. Got contradiction.
The same proof is applicable to show that if the process T1 has ended then we will not have the infinite cycle in the process T2.
Let us consider the situation where both processes T1 and T2 have infinite cycles at the same time. This situation is only possible when we observe the transitions in the following order: Tr13(S1,S2) -> Tr23(S1,S2) -> Tr13(S1,S2) -> Tr23(S1,S2) and so on. Due to Tr13(S1,S2) global variable turn = 2 while due to Tr23(S1,S2) turn = 1 ≠ 2. That means that the situation where both processes have infinite cycles is impossible.
Together with the other results (besides this work) total correctness of well-known Peterson’s Algorithm was proved. Namely, we have:
According to the wide range of difficulties of total correctness proofs in parallel environments, we may state that the IPCL method is well adapted to parallel software verification. Moreover, this method let us make the proof shorter by choosing an adequate level of abstraction of the problem due to the universality of composition-nominative languages.