Skip to content
GitLab
Menu
Projects
Groups
Snippets
Loading...
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Menu
Open sidebar
Janno
iriscoq
Commits
9ce1bdef
Commit
9ce1bdef
authored
Jun 30, 2018
by
Ralf Jung
Browse files
Allow comparing even more values in CAS by making things more consistent
parent
29c965ba
Changes
6
Hide whitespace changes
Inline
Sidebyside
tests/heap_lang.ref
View file @
9ce1bdef
...
@@ 68,11 +68,6 @@
...
@@ 68,11 +68,6 @@
let: "val2" := fun2 "val1" in
let: "val2" := fun2 "val1" in
let: "val3" := fun3 "val2" in if: "val1" = "val2" then "val" else "val3"
let: "val3" := fun3 "val2" in if: "val1" = "val2" then "val" else "val3"
{{{ (x y : val) (z : Z), RET (x, y, #z); True }}}
{{{ (x y : val) (z : Z), RET (x, y, #z); True }}}
"not_cas_compare_safe"
: string
The command has indeed failed with message:
Ltac call to "wp_cas_suc" failed.
Tactic failure: wp_cas_suc: Values are not safe to compare for CAS.
"not_cas"
"not_cas"
: string
: string
The command has indeed failed with message:
The command has indeed failed with message:
...
...
tests/heap_lang.v
View file @
9ce1bdef
...
@@ 166,13 +166,6 @@ End printing_tests.
...
@@ 166,13 +166,6 @@ End printing_tests.
Section
error_tests
.
Section
error_tests
.
Context
`
{
heapG
Σ
}.
Context
`
{
heapG
Σ
}.
Check
"not_cas_compare_safe"
.
Lemma
not_cas_compare_safe
(
l
:
loc
)
(
v
:
val
)
:
l
↦
v

∗
WP
CAS
#
l
v
v
{{
_
,
True
}}.
Proof
.
iIntros
"H↦"
.
Fail
wp_cas_suc
.
Abort
.
Check
"not_cas"
.
Check
"not_cas"
.
Lemma
not_cas
:
Lemma
not_cas
:
(
WP
#()
{{
_
,
True
}})%
I
.
(
WP
#()
{{
_
,
True
}})%
I
.
...
...
theories/heap_lang/lang.v
View file @
9ce1bdef
...
@@ 68,9 +68,6 @@ Inductive expr :=
...
@@ 68,9 +68,6 @@ Inductive expr :=
Bind
Scope
expr_scope
with
expr
.
Bind
Scope
expr_scope
with
expr
.
Notation
NONE
:
=
(
InjL
(
Lit
LitUnit
))
(
only
parsing
).
Notation
SOME
x
:
=
(
InjR
x
)
(
only
parsing
).
Fixpoint
is_closed
(
X
:
list
string
)
(
e
:
expr
)
:
bool
:
=
Fixpoint
is_closed
(
X
:
list
string
)
(
e
:
expr
)
:
bool
:
=
match
e
with
match
e
with

Var
x
=>
bool_decide
(
x
∈
X
)

Var
x
=>
bool_decide
(
x
∈
X
)
...
@@ 99,9 +96,6 @@ Inductive val :=
...
@@ 99,9 +96,6 @@ Inductive val :=
Bind
Scope
val_scope
with
val
.
Bind
Scope
val_scope
with
val
.
Notation
NONEV
:
=
(
InjLV
(
LitV
LitUnit
))
(
only
parsing
).
Notation
SOMEV
x
:
=
(
InjRV
x
)
(
only
parsing
).
Fixpoint
of_val
(
v
:
val
)
:
expr
:
=
Fixpoint
of_val
(
v
:
val
)
:
expr
:
=
match
v
with
match
v
with

RecV
f
x
e
=>
Rec
f
x
e

RecV
f
x
e
=>
Rec
f
x
e
...
@@ 122,6 +116,38 @@ Fixpoint to_val (e : expr) : option val :=
...
@@ 122,6 +116,38 @@ Fixpoint to_val (e : expr) : option val :=

_
=>
None

_
=>
None
end
.
end
.
(** We assume the following encoding of values to 64bit words: The least 3
significant bits of every word are a "tag", and we have 61 bits of payload,
which is enough if all pointers are 8bytealigned (common on 64bit
architectures). The tags have the following meaning:
0: Payload is the data for a LitV (LitInt _).
1: Payload is the data for a InjLV (LitV (LitInt _)).
2: Payload is the data for a InjRV (LitV (LitInt _)).
3: Payload is the data for a LitV (LitLoc _).
4: Payload is the data for a InjLV (LitV (LitLoc _)).
4: Payload is the data for a InjRV (LitV (LitLoc _)).
6: Payload is one of the following finitely many values, which 61 bits are more
than enough to encode:
LitV LitUnit, InjLV (LitV LitUnit), InjRV (LitV LitUnit),
LitV (LitBool _), InjLV (LitV (LitBool _)), InjRV (LitV (LitBool _)).
7: Value is boxed, i.e., payload is a pointer to some readonly memory area on
the heap which stores whether this is a RecV, PairV, InjLV or InjRV and the
relevant data for those cases. However, the boxed representation is never
used if any of the above representations could be used.
Ignoring (as usual) the fact that we have to fit the infinite Z/loc into 61
bits, this means every value is machinewordsized and can hence be atomically
read and written. Also notice that the sets of boxed and unboxed values are
disjoint. *)
Definition
val_is_unboxed
(
v
:
val
)
:
Prop
:
=
match
v
with

LitV
_
=>
True

InjLV
(
LitV
_
)
=>
True

InjRV
(
LitV
_
)
=>
True

_
=>
False
end
.
(** The state: heaps of vals. *)
(** The state: heaps of vals. *)
Definition
state
:
=
gmap
loc
val
.
Definition
state
:
=
gmap
loc
val
.
...
@@ 367,53 +393,13 @@ Definition bin_op_eval (op : bin_op) (v1 v2 : val) : option val :=
...
@@ 367,53 +393,13 @@ Definition bin_op_eval (op : bin_op) (v1 v2 : val) : option val :=

_
,
_
=>
None

_
,
_
=>
None
end
.
end
.
(** Return whether it is possible to use CAS to compare vl (current value) with
(** CAS just compares the wordsized representation of the two values, it cannot
v1 (netest value).
look into boxed data. This works out fine if at least one of the tobecompared
values is unboxed (exploiting the fact that an unboxed and a boxed value can
We assume the following encoding of values to 64bit words: The least 3
never be equal because these are disjoint sets). *)
significant bits of every word are a "tag", and we have 61 bits of payload,
which is enough if all pointers are 8bytealigned (commong on 64bit
architectures). The tags have the following meaning:
0: Payload is one of the following finitely many values, which 61 bits are more
than enough to encode: LitV LitUnit, LitV (LitBool _), NONEV, SOMEV (LitV
LitUnit), SOMEV (LitV (LitBool _)).
1: Payload is the data for a LitV (LitInt _).
2: Payload is the data for a SOMEV (LitV (LitInt _)).
3: Payload is the data for a LitV (LitLoc _).
4: Payload is the data for a SOMEV (LitV (LitLoc _)).
5: Value is boxed, i.e., payload is a pointer to some readonly memory area on
the heap which stores whether this is a RecV, PairV, InjLV or InjRV and the
relevant data for those cases. However, the boxed representation is never
used if any of the above representations could be used.
6: Unused.
7: Unused.
Ignoring (as usual) the fact that we have to fit the infinite Z/loc into 61
bits, this means every value is machinewordsized and can hence be atomically
read and written. It also justifies the comparisons allowed for CAS: Whenever
[vals_cas_compare_safe vl v1] holds, equality of the oneword representation of
[vl] and [v1] is equivalent to equality of the abstract value represented. This
is clear for [LitV _ == LitV _] and [SOMEV (LitV _) == SOMEV (LitV _)] because
none of these are boxed. For [NONEV == v], we can't actually atomically load and
compare the data for boxed values, but that's okay because we only have to know
if they are equal to [NONEV] which is distinct from all boxed values.
*)
Definition
vals_cas_compare_safe
(
vl
v1
:
val
)
:
Prop
:
=
Definition
vals_cas_compare_safe
(
vl
v1
:
val
)
:
Prop
:
=
match
vl
,
v1
with
val_is_unboxed
vl
∨
val_is_unboxed
v1
.
(* We allow comparing literals with each other, also when wrapped in a SOMEV. *)
Arguments
vals_cas_compare_safe
!
_
!
_
/.

LitV
_
,
LitV
_
=>
True

SOMEV
(
LitV
_
),
SOMEV
(
LitV
_
)
=>
True
(* We allow comparing NONEV to anything. *)

NONEV
,
_
=>
True

_
,
NONEV
=>
True
(* We don't allow comparing anything else. *)

_
,
_
=>
False
end
.
(** Just a sanity check. *)
Lemma
vals_cas_compare_safe_sym
vl
v1
:
vals_cas_compare_safe
vl
v1
→
vals_cas_compare_safe
v1
vl
.
Proof
.
rewrite
/
vals_cas_compare_safe
.
repeat
case_match
;
done
.
Qed
.
Inductive
head_step
:
expr
→
state
→
expr
→
state
→
list
(
expr
)
→
Prop
:
=
Inductive
head_step
:
expr
→
state
→
expr
→
state
→
list
(
expr
)
→
Prop
:
=

BetaS
f
x
e1
e2
v2
e'
σ
:

BetaS
f
x
e1
e2
v2
e'
σ
:
...
...
theories/heap_lang/lib/increment.v
View file @
9ce1bdef
...
@@ 39,7 +39,8 @@ Section increment.
...
@@ 39,7 +39,8 @@ Section increment.
(* Prove the atomic shift for CAS *)
(* Prove the atomic shift for CAS *)
iAuIntro
.
iApply
(
aacc_aupd
with
"AU"
)
;
first
done
.
iAuIntro
.
iApply
(
aacc_aupd
with
"AU"
)
;
first
done
.
iIntros
(
x'
)
"H↦"
.
iIntros
(
x'
)
"H↦"
.
iApply
(
aacc_intro
with
"[H↦]"
)
;
[
solve_ndisj

simpl
;
by
auto
with
iFrame

iSplit
].
iApply
(
aacc_intro
with
"[H↦]"
)
;
[
solve_ndisj


iSplit
].
{
iFrame
.
simpl
.
auto
.
}
{
iIntros
"[_ $] !> $ !> //"
.
}
{
iIntros
"[_ $] !> $ !> //"
.
}
iIntros
([])
"H↦ !>"
.
iIntros
([])
"H↦ !>"
.
destruct
(
decide
(#
x'
=
#
x
))
as
[[=
>]
Hx
].
destruct
(
decide
(#
x'
=
#
x
))
as
[[=
>]
Hx
].
...
...
theories/heap_lang/notation.v
View file @
9ce1bdef
...
@@ 144,6 +144,12 @@ Notation "e1  e2" :=
...
@@ 144,6 +144,12 @@ Notation "e1  e2" :=
(
If
e1
%
E
(
Lit
(
LitBool
true
))
e2
%
E
)
(
only
parsing
)
:
expr_scope
.
(
If
e1
%
E
(
Lit
(
LitBool
true
))
e2
%
E
)
(
only
parsing
)
:
expr_scope
.
(** Notations for option *)
(** Notations for option *)
Notation
NONE
:
=
(
InjL
(
Lit
LitUnit
))
(
only
parsing
).
Notation
SOME
x
:
=
(
InjR
x
)
(
only
parsing
).
Notation
NONEV
:
=
(
InjLV
(
LitV
LitUnit
))
(
only
parsing
).
Notation
SOMEV
x
:
=
(
InjRV
x
)
(
only
parsing
).
Notation
"'match:' e0 'with' 'NONE' => e1  'SOME' x => e2 'end'"
:
=
Notation
"'match:' e0 'with' 'NONE' => e1  'SOME' x => e2 'end'"
:
=
(
Match
e0
BAnon
e1
x
%
bind
e2
)
(
Match
e0
BAnon
e1
x
%
bind
e2
)
(
e0
,
e1
,
x
,
e2
at
level
200
,
only
parsing
)
:
expr_scope
.
(
e0
,
e1
,
x
,
e2
at
level
200
,
only
parsing
)
:
expr_scope
.
...
...
theories/heap_lang/proofmode.v
View file @
9ce1bdef
...
@@ 406,7 +406,7 @@ Tactic Notation "wp_cas_fail" :=
...
@@ 406,7 +406,7 @@ Tactic Notation "wp_cas_fail" :=
[
iSolveTC
[
iSolveTC

solve_mapsto
()

solve_mapsto
()

try
congruence

try
congruence

fast_done

fail
"wp_cas_fail: Values are not safe to compare for CAS"

try
(
fast_done

left
;
fast_done

right
;
fast_done
)
(* vals_cas_compare_safe *)

simpl
;
try
wp_value_head
]

simpl
;
try
wp_value_head
]


envs_entails
_
(
twp
?s
?E
?e
?Q
)
=>


envs_entails
_
(
twp
?s
?E
?e
?Q
)
=>
first
first
...
@@ 415,7 +415,7 @@ Tactic Notation "wp_cas_fail" :=
...
@@ 415,7 +415,7 @@ Tactic Notation "wp_cas_fail" :=

fail
1
"wp_cas_fail: cannot find 'CAS' in"
e
]
;

fail
1
"wp_cas_fail: cannot find 'CAS' in"
e
]
;
[
solve_mapsto
()
[
solve_mapsto
()

try
congruence

try
congruence

fast_done

fail
"wp_cas_fail: Values are not safe to compare for CAS"

try
(
fast_done

left
;
fast_done

right
;
fast_done
)
(* vals_cas_compare_safe *)

wp_expr_simpl
;
try
wp_value_head
]

wp_expr_simpl
;
try
wp_value_head
]

_
=>
fail
"wp_cas_fail: not a 'wp'"

_
=>
fail
"wp_cas_fail: not a 'wp'"
end
.
end
.
...
@@ 434,7 +434,7 @@ Tactic Notation "wp_cas_suc" :=
...
@@ 434,7 +434,7 @@ Tactic Notation "wp_cas_suc" :=
[
iSolveTC
[
iSolveTC

solve_mapsto
()

solve_mapsto
()

try
congruence

try
congruence

fast_done

fail
"wp_cas_suc: Values are not safe to compare for CAS"

try
(
fast_done

left
;
fast_done

right
;
fast_done
)
(* vals_cas_compare_safe *)

pm_reflexivity

pm_reflexivity

simpl
;
try
wp_value_head
]

simpl
;
try
wp_value_head
]


envs_entails
_
(
twp
?E
?e
?Q
)
=>


envs_entails
_
(
twp
?E
?e
?Q
)
=>
...
@@ 444,7 +444,7 @@ Tactic Notation "wp_cas_suc" :=
...
@@ 444,7 +444,7 @@ Tactic Notation "wp_cas_suc" :=

fail
1
"wp_cas_suc: cannot find 'CAS' in"
e
]
;

fail
1
"wp_cas_suc: cannot find 'CAS' in"
e
]
;
[
solve_mapsto
()
[
solve_mapsto
()

try
congruence

try
congruence

fast_done

fail
"wp_cas_suc: Values are not safe to compare for CAS"

try
(
fast_done

left
;
fast_done

right
;
fast_done
)
(* vals_cas_compare_safe *)

pm_reflexivity

pm_reflexivity

wp_expr_simpl
;
try
wp_value_head
]

wp_expr_simpl
;
try
wp_value_head
]

_
=>
fail
"wp_cas_suc: not a 'wp'"

_
=>
fail
"wp_cas_suc: not a 'wp'"
...
...
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