open Statement open Mapping (*Define lock as in \cite[p. 721]{Power2.06}: loop: lwarx r6,0,r3 cmpw r4,r6 bne- wait stwcx. r5,0,r3 bne- loop isync [...] wait... Define unlock as in \cite[p. 721]{Power2.06}: [...] lwsync stw r4,0,r3 *) (*Thm: Suppose that we have a Power assembly program where all competing accesses (i.e. addressing the same location, from different threads, and one of them at least is a write) to a given address x are guarded by the same lock variable l, and this for every shared-memory variable x. Then the program has a SC behaviour.*) (*Note that this means that, in the following, each event m is associated with the write L(m) of the successful stwcx. instruction of its lock primitive. Similarly, each event m is associated with the the write UL(m) of the stw of its unlock primitive.*) val locking_stwcx_of : instruction -> instruction val L : action -> action*action (*Proof: We need to prove that (po U co U rf U fr) is acyclic. By contradiction, suppose there exists x such that (x,x) is in (po U co U rf U fr)+. We show (via the lemmas below) that in this case: - (x,x) IN po, which is an immediate contradiction because po is acyclic. - (L(x),L(x)) IN RCP+, where RCP is the order in which writes from any thread and to any location reach their coherence point. Since RCP follows the machine order, it is acyclic. Thus this case is an immediate contradiction. QED Thm. *) (*Lemma: For all path (m1,m2) in (po U co U rf U fr)+, we have either L(m1) = L(m2) and (m1,m2) IN po, or (L(m1),L(m2)) IN RCP+.*) let sc_path_implies_locking_rcp_path_lemma = forall ia1 ia2. (ia1,ia2) IN tc (fr union rf union po union co) --> (snd (L ia1) = snd (L ia2) && (ia1,ia2) IN po) || ((snd(L ia1), snd(L ia2)) IN tc rcp) (*Proof: Let m1 and m2 be s.t. (m1,m2) is in (po U co U rf U fr)+, and let us reason by induction on the length of this chain. . Base case: We have (m1,m2) in (po U co U rf U fr). Let us reason by case disjunction over this statement. - Suppose (m1,m2) in po; let us do a case disjunction over whether or not they belong to the same lock. . L(m1) = L(m2): In this case, we directly have the result. . L(m1) <> L(m2): In this case, because lwarx and stwcx. instructions are committed in program order (Commit rule, Precondition 11), and since stwcx. instructions reach CP as soon as they are committed (Commit rule, Action 5 and Accept a successful write-conditional request, Action 3), we directly have (L(m1),L(m2)) IN RCP+. *) val commit_transition_of : trace let locking_in_po_reach_cp_in_order_lemma = forall ia1 ia2. (ia1,ia2) IN po --> (snd(L ia1), snd(L ia2)) IN tc rcp (* - Suppose (m1,m2) in com = co U rf U fr. If (m1,m2) in po, we apply the po case. Thus, let us assume that m1 and m2 belong to distinct threads. This means that m1 and m2 are competing, hence are guarded by the same lock variable (i.e. loc(L(m1)) = loc(L(m2))). By totality of co, we have either (L(m1),L(m2)) in co or (L(m2),L(m1)) in co. Let us do a case disjunction on this statement. _ Case (L(m1),L(m2)) IN co: In this case we directly have (L(m1),L(m2)) IN RCP+, by Write reaches its coherence point, Pre condition 2. _ Case (L(m2),L(m1)) IN co: In this case we have (UL(m2),L(m1)) IN co, because the lock primitive around m1 cannot take the lock before the unlock after m2 set it free. Let us now do a case disjunction over (m1,m2) IN co U rf U fr: *) (* + (m1,m2) IN co: In this case, m1 has been propagated to m2's thread before m2 is committed. This means (by Commit, Action 4) that m1's instruction has been committed before m2 is committed. Now, since (UL(m2),L(m1)) IN co, and because stwcx. instructions reach CP as soon as they are committed (Commit, Action 5 and Accept a successful write-conditional request, Action 3), we know that UL(m2)'s instruction is committed before L(m1)'s instruction is. Moreover, since there is a lwsync in program order between m2's instruction and UL(m2)'s instruction, we know that m2's instruction is committed before this lwsync (Commit, Pre condition 8), and that this lwsync is committed before UL(m2)'s instruction (Commit, Pre condition 5a -- should be made clear in the rule this applies to lwarx/stwcx. as well). Thus m2's instruction is committed before UL(m2)'s instruction. Finally, since there is a branch+isync in program order between L(m1)'s instruction and m1's instruction, we know by Commit, Pre condition 5a, that L(m1)'s instruction is committed before m1's instruction. Thus we contradict the machine order. *) let locking_in_co_reach_cp_in_order_lemma = forall a1 a2. (a1,a2) IN co --> (snd(L a1), snd(L a2)) IN tc rcp (* + (m1,m2) IN rf: In this case, m1 has been propagated to m2's thread before m2 is satisfied. Now, since (UL(m2),L(m1)) IN co, and because stwcx. instructions reach CP as soon as they are committed (Commit, Action 5 and Accept a successful write-conditional request, Action 3), we know that UL(m2)'s instruction is committed before L(m1)'s instruction is. Moreover, since there is a lwsync in program order between m2's instruction and UL(m2)'s instruction, we know that m2's instruction is committed (and thus m2 is satisfied, by Commit, Pre condition 1) before this lwsync (Commit, Pre condition 8), and that this lwsync is committed before UL(m2)'s instruction (Commit, Pre condition 5a -- should be made clear in the rule this applies to lwarx/stwcx. as well). Thus m2's instruction is committed before UL(m2)'s instruction. Finally, since there is a branch+isync in program order between L(m1)'s instruction and m1's instruction, we know by Commit, Pre condition 5a, that L(m1)'s instruction is committed before m1's instruction. Thus we contradict the machine order. *) let locking_in_rf_reach_cp_in_order_lemma = forall a1 a2. (a1,a2) IN rf --> (snd(L a1), snd(L a2)) IN tc rcp (* + (m1,m2) IN fr: In this case, m1 has been satisfied before to m2's instruction is committed. Now, since (UL(m2),L(m1)) IN co, and because stwcx. instructions reach CP as soon as they are committed (Commit, Action 5 and Accept a successful write-conditional request, Action 3), we know that UL(m2)'s instruction is committed before L(m1)'s instruction is. Moreover, since there is a lwsync in program order between m2's instruction and UL(m2)'s instruction, we know that m2's instruction is committed before this lwsync (Commit, Pre condition 8), and that this lwsync is committed before UL(m2)'s instruction (Commit, Pre condition 5a -- should be made clear in the rule this applies to lwarx/stwcx. as well). Thus m2's instruction is committed before UL(m2)'s instruction. Finally, since there is a branch+isync in program order between L(m1)'s instruction and m1's instruction, we know by Satisfy memory read from storage subsystem, Pre condition 4, that this isync has been committed before m1 is satisfied. Then we know by Commit, Pre condition 5a, that L(m1)'s instruction is committed before this isync, hence before m1 is satisfied. Thus we contradict the machine order. *) let locking_in_fr_reach_cp_in_order_lemma = forall a1 a2. (a1,a2) IN fr --> (snd(L a1), snd(L a2)) IN tc rcp (* . Inductive case: We have (m1,m2) in (po U co U rf U fr) and (m2,mn) in (po U co U rf U fr)+. By applying the base case to (m1,m2), we have (L(m1),L(m2)) IN RCP+, or (m1,m2) IN po and L(m1)=L(m2). Let us reason by case disjunction over this statement. . Case (L(m1),L(m2)) IN RCP+: By induction hypothesis, we have (L(m2),L(mn)) IN RCP+, or (m2,mn) IN po and L(m2)=L(mn). Let us do a case disjunction over this statement. - Suppose (L(m2),L(mn)) IN RCP+, we have (L(m1),L(mn)) IN RCP+ by transitivity of RCP. - Suppose (m2,mn) IN po and L(m2)=L(mn), then we have (L(m1),L(mn)) IN RCP+ from L(m2) = L(mn) and (L(m1),L(m2)) IN RCP+. . Case (m1,m2) IN po and L(m1)=L(m2): By induction hypothesis, we have (L(m2),L(mn)) IN RCP+, or (m2,mn) IN po and L(m2)=L(mn). Let us do a case disjunction over this statement. - Suppose (L(m2),L(mn)) IN RCP+, then we have (L(m1),L(mn)) IN RCP+ from L(m1)=L(m2) and (L(m2),L(mn)) IN RCP+. - Suppose (m2,mn) IN po and L(m2)=L(mn), then we have (m1,mn) IN po by transitivity of po and L(m1)=L(m2)=L(mn). QED Lemma. *)