Skip to content
GitLab
Menu
Projects
Groups
Snippets
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Menu
Open sidebar
Joshua Yanovski
iris-coq
Commits
0fccdf33
Commit
0fccdf33
authored
Apr 25, 2016
by
Robbert Krebbers
Browse files
Fix wrong name in lock.
parent
e5973e6f
Changes
1
Hide whitespace changes
Inline
Side-by-side
heap_lang/lib/lock.v
View file @
0fccdf33
...
@@ -5,7 +5,8 @@ Import uPred.
...
@@ -5,7 +5,8 @@ Import uPred.
Definition
newlock
:
val
:=
λ
:
<>
,
ref
#
false
.
Definition
newlock
:
val
:=
λ
:
<>
,
ref
#
false
.
Definition
acquire
:
val
:=
Definition
acquire
:
val
:=
rec:
"lock"
"l"
:=
if
:
CAS
'
"l"
#
false
#
true
then
#()
else
'
"lock"
'
"l"
.
rec:
"acquire"
"l"
:=
if:
CAS
'
"l"
#
false
#
true
then
#()
else
'
"acquire"
'
"l"
.
Definition
release
:
val
:=
λ
:
"l"
,
'
"l"
<-
#
false
.
Definition
release
:
val
:=
λ
:
"l"
,
'
"l"
<-
#
false
.
(
**
The
CMRA
we
need
.
*
)
(
**
The
CMRA
we
need
.
*
)
...
...
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
.
Attach a 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