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
adc0a095
Commit
adc0a095
authored
Dec 04, 2017
by
Robbert Krebbers
Browse files
Make `lock` instances canonical structures.
parent
48892aba
Changes
2
Hide whitespace changes
Inline
Side-by-side
theories/heap_lang/lib/spin_lock.v
View file @
adc0a095
...
...
@@ -36,7 +36,7 @@ Section proof.
Global
Instance
lock_inv_ne
γ
l
:
NonExpansive
(
lock_inv
γ
l
).
Proof
.
solve_proper
.
Qed
.
Global
Instance
is_lock_ne
l
:
NonExpansive
(
is_lock
γ
l
).
Global
Instance
is_lock_ne
γ
l
:
NonExpansive
(
is_lock
γ
l
).
Proof
.
solve_proper
.
Qed
.
(** The main proofs. *)
...
...
@@ -90,6 +90,6 @@ End proof.
Typeclasses
Opaque
is_lock
locked
.
Definition
spin_lock
`
{!
heapG
Σ
,
!
lockG
Σ
}
:
lock
Σ
:
=
Canonical
Structure
spin_lock
`
{!
heapG
Σ
,
!
lockG
Σ
}
:
lock
Σ
:
=
{|
lock
.
locked_exclusive
:
=
locked_exclusive
;
lock
.
newlock_spec
:
=
newlock_spec
;
lock
.
acquire_spec
:
=
acquire_spec
;
lock
.
release_spec
:
=
release_spec
|}.
theories/heap_lang/lib/ticket_lock.v
View file @
adc0a095
...
...
@@ -166,6 +166,6 @@ End proof.
Typeclasses
Opaque
is_lock
issued
locked
.
Definition
ticket_lock
`
{!
heapG
Σ
,
!
tlockG
Σ
}
:
lock
Σ
:
=
Canonical
Structure
ticket_lock
`
{!
heapG
Σ
,
!
tlockG
Σ
}
:
lock
Σ
:
=
{|
lock
.
locked_exclusive
:
=
locked_exclusive
;
lock
.
newlock_spec
:
=
newlock_spec
;
lock
.
acquire_spec
:
=
acquire_spec
;
lock
.
release_spec
:
=
release_spec
|}.
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