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. *)