-
Notifications
You must be signed in to change notification settings - Fork 9
/
wmm.v
133 lines (103 loc) · 5.38 KB
/
wmm.v
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
(*********************************************************************)
(* A Formal Hierarchy of Weak Memory Models *)
(* *)
(* Jade Alglave INRIA Paris-Rocquencourt, France. *)
(* *)
(* Copyright 2010 Institut National de Recherche en Informatique et *)
(* en Automatique. All rights reserved. This file is distributed *)
(* under the terms of the Lesser GNU General Public License. *)
(*********************************************************************)
(******************************************************************************)
(* PipeCheck: Specifying and Verifying Microarchitectural *)
(* Enforcement of Memory Consistency Models *)
(* *)
(* Copyright (c) 2014 Daniel Lustig, Princeton University *)
(* All rights reserved. *)
(* *)
(* This library is free software; you can redistribute it and/or *)
(* modify it under the terms of the GNU Lesser General Public *)
(* License as published by the Free Software Foundation; either *)
(* version 2.1 of the License, or (at your option) any later version. *)
(* *)
(* This library is distributed in the hope that it will be useful, *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU *)
(* Lesser General Public License for more details. *)
(* *)
(* You should have received a copy of the GNU Lesser General Public *)
(* License along with this library; if not, write to the Free Software *)
(* Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA 02110-1301 *)
(* USA *)
(******************************************************************************)
(******************************************************************************)
(* This file contains the pieces of Alglave's CAV 2010 Weak Memory Model *)
(* analysis framework that have been adapted for use in PipeCheck. The full *)
(* contents of the original framework are available at *)
(* http://www0.cs.ucl.ac.uk/staff/j.alglave/wmm *)
(******************************************************************************)
Set Implicit Arguments.
(** * Basic types *)
(** ** Words *)
(** We abstract from word-size and alignment issues for now,
modelling both memory addresses and the values that may be
stored in them by natural numbers. *)
Definition Word := nat.
(** *** Addresses *)
Definition Address := Word.
(** *** Values *)
Definition Value := Word.
(** ** Processors *)
(** Processors are indexed by natural numbers. *)
Definition Proc := nat.
(** The model is expressed in terms of allowable orderings on events:
individual reads and writes to memory, and
memory barrier events. Each instance of an instruction in a
program execution may give rise to multiple events, as described
by the instruction semantics. We abstract from
the details of instructions, but we record in each event the
instruction instance id (an iiid) that gave rise to it, so that
we can refer to the program order over the instruction
instances. An instruction instance id specifies the processor
on which the instruction was executed together with the index of
the program-order point at which it was executed (represented by
a natural number).*)
(** ** Index in program order *)
Definition program_order_index := nat.
(** ** Iiid: instruction identifier *)
Record Iiid : Set := mkiiid {
proc : Proc;
poi: program_order_index }.
(** Each event has an event instance id (eiid), the associated
instruction instance id (iiid), and an action. An action is
either an access, with a direction (read or write),
a memory location specified by an address, and a value. *)
(** ** Eiid: unique event identifier *)
Definition Eiid := nat.
(** ** Directions
i.e. read or write*)
Inductive Dirn : Set :=
| R : Dirn
| W : Dirn.
(** ** Location:
- a memory location is specified by an address*)
Definition Location := Address.
(** ** Action:
- an access specified by a polarity, a location and a value *)
Inductive Action : Set :=
| Access : Dirn -> Location -> Value -> Action.
(** ** Event:
- an unique identifier;
- the associated index in program order and the proc;
- the associated action *)
Record Event : Set := mkev {
eiid : Eiid;
iiid : Iiid;
action : Action}.
Definition dirn (e : Event) : Dirn :=
match e with mkev _ _ (Access d _ _) => d end.
(** * Basic operations on data types *)
(** ** Location of an event *)
Definition loc (e:Event) : (*option*) Location :=
match e.(action) with
| Access _ l _ => (*Some*) l
end.