(* A draft mechanization of some of Manson and Pugh's draft memory models for Java
* Created by Bart Jacobs (http://www.cs.kuleuven.be/~bartj/), August 2003
*
* Typechecked using Isabelle2003/HOL (http://isabelle.in.tum.de/)
*)
theory JavaMemoryModel = Main:
text {*
Note: the English text is for clarification only;
it is not intended to be precise or rigorous.
*}
section {* Programs *}
subsection {* Statements *}
datatype statement =
Compute nat "nat list => nat" "nat list"
| FieldUse nat nat
| FieldAssign nat nat
| Enter nat
| Exit nat
datatype action =
NoOp
| ComputeAction
| FieldUseAction nat nat
| FieldAssignAction nat nat
| EnterAction nat
| ExitAction nat
types thread_result = "nat => nat"
constdefs
statement_semantics :: "statement => nat => thread_result => (action * thread_result)"
"statement_semantics s fur r ==
(case s of
Compute k f as => (ComputeAction, r(k:=f (map r as)))
| FieldUse k i => (FieldUseAction i fur, r(k:=fur))
| FieldAssign i k => (FieldAssignAction i (r k), r)
| Enter i => (EnterAction i, r)
| Exit i => (ExitAction i, r))"
text {*
A thread has an infinite number of registers.
The natural numbers serve as the names of registers.
The natural numbers also serve as the values of registers.
A thread result is a mapping of register names onto register values.
Semantically, a statement takes a thread result and produces an action, as well as a new thread result.
All this is parameterized by a field use result (fur).
A compute statement takes a target register name, a function, and a list of source register names.
For example, suppose \texttt{sum} is a function that returns the sum of its arguments.
Then \texttt{(Compute 0 sum [0, 1])} is a statement that assigns the sum of the contents of
registers 0 and 1 to register 0.
A field use statement assigns the field use result associated with the statement to the named register.
It also produces a field use action.
*}
subsection {* Steps *}
types program_step = "nat option * statement"
constdefs
step_semantics :: "program_step => nat => thread_result => (action * thread_result)"
"step_semantics step fur r ==
(let
(C, stmt) = step
in
(if (case C of None => True | Some k => 0 < r k) then
statement_semantics stmt fur r
else
(NoOp, r)))"
text {*
A step consists of an optional condition, and a statement.
The condition, if present, is a register name.
The condition is satisfied if the named register is nonzero.
If the condition is not satisfied, the step produces a no-op action.
Each step produces exactly one action.
*}
subsection {* Threads and Programs *}
types thread_program = "program_step list"
types thread_field_use_results = "nat list"
constdefs
thread_program_semantics :: "thread_program => thread_field_use_results => (action list * thread_result)"
"thread_program_semantics p furs ==
foldl (%(as, r) (step, fur). (let (a, r) = step_semantics step fur r in (as @ [a], r))) ([], (%k. 0)) (zip p furs)"
types program = "thread_program list"
types program_result = "thread_result list"
types program_field_use_results = "thread_field_use_results list"
constdefs
intra_thread_semantics :: "program => program_field_use_results => (action list list * program_result)"
"intra_thread_semantics P furs ==
(let sem = map (%(p, furs). thread_program_semantics p furs) (zip P furs) in (map fst sem, map snd sem))"
types memory_model = "program => program_field_use_results => bool"
text {*
A memory model is a predicate over pairs of programs and program field use results.
*}
section {* Consistency *}
types action_id = "nat * nat"
types action_order = "(action_id * action_id) set"
subsection {* Happens-before *}
constdefs
happens_before :: "action list list => action_order => bool"
"happens_before A hb ==
(let
actions = {(m, n). m < length A & n < length (A ! m)}
in
(EX lo.
(ALL i.
set (lo i) = {(m, n). (m, n) : actions & (A ! m ! n = EnterAction i | A ! m ! n = ExitAction i)} &
(ALL j j'.
j < length (lo i) -->
j' < length (lo i) -->
j < j' -->
fst (lo i ! j) = fst (lo i ! j') -->
snd (lo i ! j) < snd (lo i ! j')) &
(let
level = foldl (%l (m, n). if A ! m ! n = EnterAction i then Suc l else inv Suc l) 0
in
(ALL j.
j < length (lo i) -->
0 < level (take j (lo i)) -->
snd (lo i ! j) = snd (lo i ! Suc j)))) &
(let
hb1 = {((m, n), (m, Suc n)) | m n. m < length A & Suc n < length (A ! m)};
hb2 = {(lo i ! j, lo i ! Suc j) | i j. Suc j < length (lo i)}
in
~ (EX a. (a, a) : hb) &
hb = (hb1 Un hb2)^+)))"
text {*
A happens-before relation is the transitive closure of the union of two sets of edges:
the edges from statements to their successors in the program,
and the edges from synchronization actions to their successors in the total order
over the synchronization actions pertaining to the same lock.
Each of these total orders must obey mutual exclusion.
A total order is represented as a list.
*}
subsection {* Allowed reads *}
constdefs
fielduseactions_allowed :: "action list list => action_order => bool"
"fielduseactions_allowed A order ==
(let
actions = {(m, n). m < length A & n < length (A ! m)}
in
(ALL m n i v.
(m, n) : actions -->
A ! m ! n = FieldUseAction i v -->
(op |
(EX (m', n'):actions.
A ! m' ! n' = FieldAssignAction i v &
((m, n), (m', n')) ~: order &
~ (EX m'' n'' v''.
(m'', n'') : actions &
A ! m'' ! n'' = FieldAssignAction i v'' &
((m', n'), (m'', n'')) : order &
((m'', n''), (m, n)) : order))
(v = 0 &
~ (EX m' n' v'.
(m', n') : actions &
A ! m' ! n' = FieldAssignAction i v' &
((m', n'), (m, n)) : order)))))"
text {*
A read (i.e. a field use action) is allowed if either
\begin{itemize}
\item
there is a write of the same value that does not happen after the read and that is not overwritten by another write, or
\item
the value read is zero, and no write happens before the read.
\end{itemize}
*}
constdefs
consistency :: memory_model
"consistency P furs ==
(let
A = fst (intra_thread_semantics P furs)
in
(EX hb.
happens_before A hb &
fielduseactions_allowed A hb))"
section {* Correctly synchronized programs *}
constdefs
data_race :: "action list list => action_order => action_id => action_id => bool"
"data_race ==
(%A hb (m1, n1) (m2, n2).
(? i v1 v2.
(A ! m1 ! n1 = FieldUseAction i v1 | A ! m1 ! n1 = FieldAssignAction i v1) &
(A ! m2 ! n2 = FieldUseAction i v2 | A ! m2 ! n2 = FieldAssignAction i v2) &
(A ! m1 ! n1 = FieldAssignAction i v1 | A ! m2 ! n2 = FieldAssignAction i v2) &
((m1, n1), (m2, n2)) ~: hb &
((m2, n2), (m1, n1)) ~: hb))"
constdefs
sequentially_consistent_execution :: "action list list => action_order => bool"
"sequentially_consistent_execution A hb ==
(EX seq.
set seq = {(m, n). m < length A & n < length (A ! m)} &
distinct seq &
(let
order = {(seq ! j, seq ! Suc j) | j. Suc j < length seq}^+
in
hb <= order &
fielduseactions_allowed A order))"
text {*
An execution is sequentially consistent if there is some total
order over all actions, that is consistent with the happens-before relation
and under which all reads are allowed.
*}
constdefs
sequential_consistency :: memory_model
"sequential_consistency P furs ==
(let
A = fst (intra_thread_semantics P furs)
in
(EX hb.
happens_before A hb &
sequentially_consistent_execution A hb))"
constdefs
correctly_synchronized :: "program => bool"
"correctly_synchronized P ==
(ALL furs hb.
length furs = length P -->
(ALL (furs, p):set (zip furs P). length furs = length p) -->
(let
A = fst (intra_thread_semantics P furs);
actions = {(m, n). m < length A & n < length (A ! m)}
in
happens_before A hb -->
sequentially_consistent_execution A hb -->
(ALL a1 a2.
a1 : actions --> a2 : actions --> a1 ~= a2 -->
~ data_race A hb a1 a2)))"
section {* Causality *}
constdefs
prescient :: "action list list => action_order => action_id list => nat => bool"
"prescient A hb co i ==
op |
(EX j.
j < length co &
i < j &
(co ! j, co ! i) : hb)
(EX j v m n.
co ! i = (m, n) &
A ! m ! n = FieldUseAction j v &
~ (EX i' m' n'.
i' < i &
co ! i = (m', n') &
A ! m' ! n' = FieldAssignAction j v &
((m, n), (m', n')) ~: hb &
~ (EX m'' n'' v''.
m'' < length A &
n'' < length (A ! m'') &
A ! m'' ! n'' = FieldAssignAction j v'' &
((m', n'), (m'', n'')) : hb &
((m'', n''), (m', n')) : hb)) &
~ (v = 0 &
~ (EX m' n' v'.
m' < length A &
n' < length (A ! n') &
A ! m' ! n' = FieldAssignAction j v' &
((m', n'), (m, n)) : hb)))"
text {*
An action is prescient, if either
\begin{itemize}
\item
there is another action that occurs later in the causal order, but earlier in the happens-before order, or
\item
the action is a read and and it is not allowed to read either the initial value or a write that occurred earlier
in the causal order
\end{itemize}
*}
constdefs
correspondence :: "action list list => action_order => action_id list => nat => action list list => action_order => action_id list => nat => bool"
"correspondence A hb co k A' hb' co' k' ==
(ALL i < k.
A ! fst (co ! i) ! snd (co ! i) = A' ! fst (co' ! i) ! snd (co' ! i) &
(ALL (j, j'):{(j, j). i < j & j < k} Un {(k, k')}.
((co ! i, co ! j) : hb) = ((co' ! i, co' ! j') : hb) &
((co ! j, co ! i) : hb) = ((co' ! j', co' ! i) : hb)))"
constdefs
execution_contains :: "action list list => action_order => action_id list => action list list => action_order => action_id list => bool"
"execution_contains A hb co A' hb' co' ==
(ALL i < length co.
correspondence A hb co i A' hb' co' i &
A ! fst (co ! i) ! snd (co ! i) = A' ! fst (co' ! i) ! snd (co' ! i))"
constdefs
strong_correspondence :: "action list list => action_order => action_id list => nat => action list list => action_order => action_id list => nat => bool"
"strong_correspondence A hb co i A' hb' co' i' ==
correspondence A hb co i A' hb' co' i' &
(let
(m, n) = co ! i;
a = A ! m ! n;
(m', n') = co' ! i';
a' = A' ! m' ! n'
in
(ALL j v.
if a = FieldUseAction j v then
(EX v'.
a' = FieldUseAction j v' &
(op |
(EX i'' m'' n''.
i'' < length co' &
(m'', n'') = co' ! i'' &
A' ! m'' ! n'' = FieldAssignAction j v &
((m', n'), (m'', n'')) ~: hb' &
~ (EX i''' m''' n''' v'''.
i''' < length co' &
(m''', n''') = co' ! i''' &
A' ! m''' ! n''' = FieldAssignAction j v''' &
((m'', n''), (m''', n''')) : hb' &
((m''', n'''), (m', n')) : hb'))
(v = 0 &
~ (EX i'' m'' n'' v''.
i'' < length co' &
(m'', n'') = co' ! i'' &
A' ! m'' ! n'' = FieldAssignAction j v'' &
((m'', n''), (m', n')) : hb))))
else
a = a'))"
text {*
There is strong correspondence between two actions if
there is correspondence and either the actions are
equal or they are reads of the same field and the right-hand-side read
is allowed to read the same value as the left-hand-side read.
*}
constdefs
strong_causality :: memory_model
"strong_causality P furs ==
(let
A = fst (intra_thread_semantics P furs);
actions = {(m, n). m < length A & n < length (A ! m)}
in
(EX hb.
happens_before A hb &
fielduseactions_allowed A hb &
(EX co.
set co = actions &
distinct co &
(ALL i.
i < length co -->
prescient A hb co i -->
(let
J = {(A', hb', a' @ b') | A' hb' a' b' furs'.
length furs' = length P &
(ALL (furs, p) : set (zip furs P). length furs = length p) &
A' = fst (intra_thread_semantics P furs') &
happens_before A' hb' &
fielduseactions_allowed A' hb' &
set (a' @ b') = actions &
distinct (a' @ b') &
length a' = i &
~ (EX i'. i <= i' & i' < length (a' @ b') & prescient A' hb' (a' @ b') i') &
execution_contains A hb (take i co) A' hb' (a' @ b')}
in
(EX Proh.
Proh <= J &
(ALL (A', hb', co'):J - Proh.
(EX i'. i <= i' & i' < length co & strong_correspondence A hb co i A' hb' co' i')) &
(ALL (Ap, hbp, cop):Proh.
(EX ip mp np jp vp i' m' n' v'.
ip < length cop &
cop ! ip = (mp, np) &
Ap ! mp ! np = FieldUseAction jp vp &
(EX (A', hb', co'):J - Proh.
ip <= i' &
i' < length co' &
co' ! i' = (m', n') &
A' ! m' ! n' = FieldUseAction jp v' &
execution_contains Ap hbp (take ip cop) A' hb' (take i' co') &
strong_correspondence Ap hbp cop ip A' hb' co' i' &
vp ~= v')))))))))"
text {*
An execution is allowed by strong causality
if each prescient action can be justified.
Consider all potential justifying executions. These proceed without prescient actions.
Each of these executions must be discharged by either showing that there is strong correspondence,
or by showing that some read occurs that strongly corresponds with an execution with which there is strong correspondence.
*}
end