(* 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