Skip to content
GitLab
Projects
Groups
Snippets
/
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Menu
Open sidebar
Rodolphe Lepigre
Iris
Commits
408b55f0
Commit
408b55f0
authored
Jun 20, 2019
by
Ralf Jung
Browse files
comment nits
parent
12bec4d5
Changes
2
Hide whitespace changes
Inline
Side-by-side
theories/heap_lang/lang.v
View file @
408b55f0
...
...
@@ -97,7 +97,7 @@ Inductive expr :=
|
AllocN
(
e1
e2
:
expr
)
(* array length (positive number), initial value *)
|
Load
(
e
:
expr
)
|
Store
(
e1
:
expr
)
(
e2
:
expr
)
|
CmpXchg
(
e0
:
expr
)
(
e1
:
expr
)
(
e2
:
expr
)
|
CmpXchg
(
e0
:
expr
)
(
e1
:
expr
)
(
e2
:
expr
)
(* Compare-exchange *)
|
FAA
(
e1
:
expr
)
(
e2
:
expr
)
(* Fetch-and-add *)
(* Prophecy *)
|
NewProph
...
...
theories/heap_lang/notation.v
View file @
408b55f0
...
...
@@ -25,7 +25,7 @@ Notation LetCtx x e2 := (AppRCtx (LamV x e2)) (only parsing).
Notation
SeqCtx
e2
:
=
(
LetCtx
BAnon
e2
)
(
only
parsing
).
Notation
Match
e0
x1
e1
x2
e2
:
=
(
Case
e0
(
Lam
x1
e1
)
(
Lam
x2
e2
))
(
only
parsing
).
Notation
Alloc
e
:
=
(
AllocN
(
Val
$
LitV
$
LitInt
1
)
e
)
(
only
parsing
).
(** Compare-and-set (CAS) retur
s
n just a boolean indicating success or failure. *)
(** Compare-and-set (CAS) return
s
just a boolean indicating success or failure. *)
Notation
CAS
l
e1
e2
:
=
(
Snd
(
CmpXchg
l
e1
e2
))
(
only
parsing
).
(* Skip should be atomic, we sometimes open invariants around
...
...
Write
Preview
Supports
Markdown
0%
Try again
or
attach a new file
.
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment