open Atomic_deadlock let no_vsse_cpp_memory_model opsem (p : 'program) = let executions = { (actions,threads,lk,sb,asw,dd,cd,rf,mo,sc,lo) | opsem p actions threads lk sb asw dd cd && no_vsse_consistent_execution actions threads lk sb asw dd cd rf mo sc lo } in if (exist (ex IN executions) actions threads lk sb asw dd cd rf mo sc lo. (ex = (actions,threads,lk,sb,asw,dd,cd,rf,mo,sc,lo)) --> not (indeterminate_reads actions rf = {}) && not (unsequenced_races actions sb = {}) && not (data_races' actions threads lk sb asw dd cd rf mo sc lo = {}) && not (bad_mutexes actions lk sb lo = {}) ) then None else Some executions let no_vsse_multi_lo_cpp_memory_model opsem (p : 'program) = let executions = { (actions,threads,lk,sb,asw,dd,cd,rf,mo,sc,lo) | opsem p actions threads lk sb asw dd cd && no_vsse_multi_lo_consistent_execution actions threads lk sb asw dd cd rf mo sc lo } in if (exist (ex IN executions) actions threads lk sb asw dd cd rf mo sc lo. (ex = (actions,threads,lk,sb,asw,dd,cd,rf,mo,sc,lo)) --> not (indeterminate_reads actions rf = {}) && not (unsequenced_races actions sb = {}) && not (data_races' actions threads lk sb asw dd cd rf mo sc lo = {}) && not (bad_mutexes actions lk sb lo = {}) ) then None else Some executions let no_vsse_multi_lo_single_sw_cpp_memory_model opsem (p : 'program) = let executions = { (actions,threads,lk,sb,asw,dd,cd,rf,mo,sc,lo) | opsem p actions threads lk sb asw dd cd && no_vsse_multi_lo_single_sw_consistent_execution actions threads lk sb asw dd cd rf mo sc lo } in if (exist (ex IN executions) actions threads lk sb asw dd cd rf mo sc lo. (ex = (actions,threads,lk,sb,asw,dd,cd,rf,mo,sc,lo)) --> not (indeterminate_reads actions rf = {}) && not (unsequenced_races actions sb = {}) && not (data_races' actions threads lk sb asw dd cd rf mo sc lo = {}) && not (bad_mutexes actions lk sb lo = {}) ) then None else Some executions (* --- Lemma 1 --- The behaviours allowed by the single lock order model are precisely the same as the multi-lock-order model. *) let Lemma1 opsem = forall p. (no_vsse_multi_lo_cpp_memory_model opsem p = no_vsse_cpp_memory_model opsem p) (* --- Proof 1 --- The proof is separated into two directions: 1. A particular consistent_execution in the single lock order model is also consistent in the multi-lock order model, and the races are precisely the same. 2. Given a consistent execution in the multi-lock-order model, we can construct a lock order that makes the other relations a consistent_execution, or construct a possibly-different consistent_execution with a race. -- Part 1 -- If we have a consistent_execution, we must construct a multi_lo_consistent_execution. Take the edges of lo relating actions on the same location and use them to make the multi-location lock order mlo. Keep all other relations the same and show that this is a multi_lo_consistent_execution. well_formed_threads has not changed, so is still satisfied. We will know most of the other predicates if we can show that happens-before has not changed. The only part that is different is synchronizes_with, which now takes mlo rather than lo. By inspection, we see that synchronization depends on lo edges that relate actions on the same location, precisely the edges still in mlo. Consequently, sw is the same, and so are the rest of the predicates dependent on it. This leaves us to consider multi_lo_consistent_locks. We have consistent_locks for lo, so we know lo agrees with hb. Because hb is the same and mlo is a subset of lo, we know that mlo agrees with hb as well. All edges with relating lock actions on the same location are included in mlo from lo, so we have the existence of an intervening unlock in mlo between two successful locks at the same location. Finally, lo was a strict total order over all mutex actions, by restricting it to same-location edges, we make it a per location total order of actions at mutex locations, this relies on actions_respect_location_kinds. To show the racy part, it is sufficient to observe that bad mutexes is identical in the two models and furthermore, only ever uses the lock order restricted to a single location. -- Part 2 -- If we have a multi_lo_consistent_execution, we can construct a lock order that makes the other relations a consistent_execution, or construct a possibly-different consistent_execution with a race. We will prove this by constructing a total lock order, lo, that contains mlo and is part of a consistent_execution. In order to do this we need to show that there are no cycles in (mlo U hb)*. There are no sb successors of blocked locks by multi_lo_consistent_execution, and no synchronisation arising from them either, so if a blocked lock is part of a cycle, it must be an intervening lock in mlo between two other actions. Because mlo is transitive, if there are no cycles over the subset of the actions without blocked locks, then there are no cycles in the general case. Let mlo' be mlo restricted to remove blocking locks. Two actions are adjacent in a relation if they are related and there is no intervening action that is related between. Take an arbitrary linearisation of hb, hb'. Any cycle (excluding blocked locks) must have at least one mlo' edge that opposes hb'. We will prove acyclicity by inducting on the length of a prefix of hb'. Start with a prefix of length N that contains no mlo' edges that oppose hb'. Now consider the prefix of length N+1. Assume the new action is part of an mlo' edge that opposes hb'. The action could therefore be an unlock, or a successful lock, consider each in turn. - unlock - If the mlo' edge terminates at a lock, then there is a synchronisation edge and we have an hb edge that disagrees with hb', a contradiction. If the mlo' edge terminates at an unlock, then truncate the prefix at N+1 and complete a multi_lo_consistent_execution according to the operational semantics in such a way that all hb' successors of action N+1 are mlo successors as well. A simple way to do this would be to have all locks block, then the consistency requirements disappear for mutexes. Now the opposing mlo' edge is adjacent and constitutes an instance of bad_mutex_use, so the the program has undefined behaviour in the multi-lock-order model. Take the N+1-prefix again and complete a consistent_execution according to the operational semantics in such a way that all hb' successors of action N+1 are lo successors as well. Then this execution also has bad_mutex_use and therefore the program has undefined behaviour in the single lock order model. - successful lock - If the mlo' edge terminates at a lock then there must be an intervening unlock because the multi-lock-order execution is consistent. The unlock must be after both locks in hb'. The unlock synchronizes with the second lock in mlo' oposing hb' giving a contradiction. If the mlo' edge terminates at an unlock then truncate the prefix at N+1 and complete a multi_lo_consistent_execution according to the operational semantics in such a way that all hb' successors of action N+1 are mlo successors as well. Now the opposing mlo' edge is adjacent. There cannot be an sb edge against hb', from the lock to the unlock, so this is an instance of bad_mutex_use. Take the N+1-prefix again and complete a consistent_execution according to the operational semantics in such a way that all hb' successors of action N+1 are lo successors as well. Again this is bad_mutex_use. So the above shows that there are no cycles and we can indeed linearise mlo into lo in such a way that agrees with happens before. The remaining conditions in consistent_execution are clearly true by inspection, similar to before. --- Lemma 2 --- In the model with unlocks synchronising with all following locks in mlo and the model where they only synchronise with the next lock in mlo, either happens before is precisely the same for a given execution, or the program has undefined behaviour in both models. *) let Lemma2 opsem = forall p. (no_vsse_multi_lo_cpp_memory_model opsem p = no_vsse_multi_lo_single_sw_cpp_memory_model opsem p) (* --- Proof 2 --- Build the full hb from the less synchronised model and show they are the same. A consistent per location lock order without undefined behaviour must have: - an intervening unlock between each pair of locks - synchronisation from each unlock to the next lock - a lock sb each unlock, adjacent in mlo - no successful lock adjacent to any other successful lock in mlo We need to show that an arbitrary unlock happens before an arbitrary lock that is later in mlo. Blocking locks don't interact so consider mlo' that doesn't have them. If there are no locks later in mlo', we are done. Otherwise the unlock synchronises with the next lock. Either we are finished, or there is an sb edge to another unlock, and we can repeat the process. Because mlo' has finite prefixes, we will finish. *)