Commit f5defba3 authored by Ralf Jung's avatar Ralf Jung

Merge branch 'ralf/cas' into 'gen_proofmode'

Allow comparing even more values in CAS by adding non-determinism

See merge request FP/iris-coq!167
parents f8e23d1c 78b2c0ef
......@@ -68,11 +68,6 @@
let: "val2" := fun2 "val1" in
let: "val3" := fun3 "val2" in if: "val1" = "val2" then "val" else "val3"
{{{ (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"
: string
The command has indeed failed with message:
......
......@@ -116,6 +116,13 @@ Section tests.
P - ( Q Φ, Q - WP e {{ Φ }}) - WP e {{ _, True }}.
Proof. iIntros "HP HW". wp_apply "HW". iExact "HP". Qed.
Lemma wp_cas l v :
val_is_unboxed v
l v - WP CAS #l v v {{ _, True }}.
Proof.
iIntros (?) "?". wp_cas as ? | ?. done. done.
Qed.
End tests.
Section printing_tests.
......@@ -166,13 +173,6 @@ End printing_tests.
Section error_tests.
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".
Lemma not_cas :
(WP #() {{ _, True }})%I.
......
......@@ -68,9 +68,6 @@ Inductive 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 :=
match e with
| Var x => bool_decide (x X)
......@@ -99,9 +96,6 @@ Inductive 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 :=
match v with
| RecV f x e => Rec f x e
......@@ -122,6 +116,38 @@ Fixpoint to_val (e : expr) : option val :=
| _ => None
end.
(** We assume the following encoding of values to 64-bit 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 8-byte-aligned (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 read-only 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 machine-word-sized 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. *)
Definition state := gmap loc val.
......@@ -367,53 +393,13 @@ Definition bin_op_eval (op : bin_op) (v1 v2 : val) : option val :=
| _, _ => None
end.
(** Return whether it is possible to use CAS to compare vl (current value) with
v1 (netest value).
We assume the following encoding of values to 64-bit 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 8-byte-aligned (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 read-only 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 machine-word-sized 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 one-word 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.
*)
(** CAS just compares the word-sized representation of the two values, it cannot
look into boxed data. This works out fine if at least one of the to-be-compared
values is unboxed (exploiting the fact that an unboxed and a boxed value can
never be equal because these are disjoint sets). *)
Definition vals_cas_compare_safe (vl v1 : val) : Prop :=
match vl, v1 with
(* We allow comparing literals with each other, also when wrapped in a SOMEV. *)
| 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.
val_is_unboxed vl val_is_unboxed v1.
Arguments vals_cas_compare_safe !_ !_ /.
Inductive head_step : expr state expr state list (expr) Prop :=
| BetaS f x e1 e2 v2 e' σ :
......
......@@ -33,11 +33,15 @@ Structure atomic_heap {Σ} `{!heapG Σ} := AtomicHeap {
(λ v, mapsto l 1 v)
(λ v (_:()), mapsto l 1 w)
(λ _ _, #()%V);
(* This spec is slightly weaker than it could be: It is sufficient for [w1]
*or* [v] to be unboxed. However, by writing it this way the [val_is_unboxed]
is outside the atomic triple, which makes it much easier to use -- and the
spec is still good enough for all our applications. *)
cas_spec (l : loc) (e1 e2 : expr) (w1 w2 : val) :
IntoVal e1 w1 IntoVal e2 w2
IntoVal e1 w1 IntoVal e2 w2 val_is_unboxed w1
atomic_wp (cas (#l, e1, e2))%E
(λ v, vals_cas_compare_safe v w1 mapsto l 1 v)%I
(λ v, mapsto l 1 v)%I
(λ v (_:()), if decide (v = w1) then mapsto l 1 w2 else mapsto l 1 v)
(λ v _, #(if decide (v = w1) then true else false)%V);
}.
......@@ -88,16 +92,16 @@ Section proof.
Qed.
Lemma primitive_cas_spec (l : loc) e1 e2 (w1 w2 : val) :
IntoVal e1 w1 IntoVal e2 w2
IntoVal e1 w1 IntoVal e2 w2 val_is_unboxed w1
atomic_wp (primitive_cas (#l, e1, e2))%E
(λ v, vals_cas_compare_safe v w1 l v)%I
(λ v, l v)%I
(λ v (_:()), if decide (v = w1) then l w2 else l v)%I
(λ v _, #(if decide (v = w1) then true else false)%V).
Proof.
iIntros (<- <- Q Φ) "? AU". wp_let. repeat wp_proj.
iMod (aupd_acc with "AU") as (v) "[[% H↦] [_ Hclose]]"; first solve_ndisj.
destruct (decide (v = w1)) as [Hv|Hv]; [wp_cas_suc|wp_cas_fail];
iIntros (<- <- ? Q Φ) "? AU". wp_let. repeat wp_proj.
iMod (aupd_acc with "AU") as (v) "[H↦ [_ Hclose]]"; first solve_ndisj.
destruct (decide (v = w1)) as [<-|Hv]; [wp_cas_suc|wp_cas_fail];
iMod ("Hclose" $! () with "H↦") as "HΦ"; by iApply "HΦ".
Qed.
......
......@@ -35,12 +35,12 @@ Section increment.
iIntros ([]) "$ !> AU !> HQ".
(* Now go on *)
wp_let. wp_op. wp_bind (aheap.(cas) _)%I.
wp_apply (cas_spec with "[HQ]"); first by iAccu.
wp_apply (cas_spec with "[HQ]"); first done; first by iAccu.
(* Prove the atomic shift for CAS *)
iAuIntro. iApply (aacc_aupd with "AU"); first done.
iIntros (x') "H↦".
iApply (aacc_intro with "[H↦]"); [solve_ndisj|simpl;by auto with iFrame|iSplit].
{ iIntros "[_ $] !> $ !> //". }
iApply (aacc_intro with "[H↦]"); [solve_ndisj|done|iSplit].
{ eauto 10 with iFrame. }
iIntros ([]) "H↦ !>".
destruct (decide (#x' = #x)) as [[= ->]|Hx].
- iRight. iExists (). iFrame. iIntros "HΦ !> HQ".
......
......@@ -144,6 +144,12 @@ Notation "e1 || e2" :=
(If e1%E (Lit (LitBool true)) e2%E) (only parsing) : expr_scope.
(** 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'" :=
(Match e0 BAnon e1 x%bind e2)
(e0, e1, x, e2 at level 200, only parsing) : expr_scope.
......
......@@ -221,10 +221,49 @@ Proof.
rewrite right_id. by apply sep_mono_r, wand_mono.
Qed.
Lemma tac_wp_cas Δ Δ' Δ'' s E i K l v e1 v1 e2 v2 Φ :
IntoVal e1 v1 IntoVal e2 v2
MaybeIntoLaterNEnvs 1 Δ Δ'
envs_lookup i Δ' = Some (false, l v)%I
envs_simple_replace i false (Esnoc Enil i (l v2)) Δ' = Some Δ''
vals_cas_compare_safe v v1
(v = v1 envs_entails Δ'' (WP fill K (Lit (LitBool true)) @ s; E {{ Φ }}))
(v v1 envs_entails Δ' (WP fill K (Lit (LitBool false)) @ s; E {{ Φ }}))
envs_entails Δ (WP fill K (CAS (Lit (LitLoc l)) e1 e2) @ s; E {{ Φ }}).
Proof.
rewrite envs_entails_eq=> ?????? Hsuc Hfail. destruct (decide (v = v1)) as [<-|Hne].
- rewrite -wp_bind. eapply wand_apply; first exact: wp_cas_suc.
rewrite into_laterN_env_sound -later_sep /= {1}envs_simple_replace_sound //; simpl.
apply later_mono, sep_mono_r. rewrite right_id. apply wand_mono; auto.
- rewrite -wp_bind. eapply wand_apply.
{ eapply wp_cas_fail; eauto. by eexists. }
rewrite into_laterN_env_sound -later_sep /= {1}envs_lookup_split //; simpl.
apply later_mono, sep_mono_r. apply wand_mono; auto.
Qed.
Lemma tac_twp_cas Δ Δ' s E i K l v e1 v1 e2 v2 Φ :
IntoVal e1 v1 IntoVal e2 v2
envs_lookup i Δ = Some (false, l v)%I
envs_simple_replace i false (Esnoc Enil i (l v2)) Δ = Some Δ'
vals_cas_compare_safe v v1
(v = v1 envs_entails Δ' (WP fill K (Lit (LitBool true)) @ s; E [{ Φ }]))
(v v1 envs_entails Δ (WP fill K (Lit (LitBool false)) @ s; E [{ Φ }]))
envs_entails Δ (WP fill K (CAS (Lit (LitLoc l)) e1 e2) @ s; E [{ Φ }]).
Proof.
rewrite envs_entails_eq=> ????? Hsuc Hfail. destruct (decide (v = v1)) as [<-|Hne].
- rewrite -twp_bind. eapply wand_apply; first exact: twp_cas_suc.
rewrite /= {1}envs_simple_replace_sound //; simpl.
apply sep_mono_r. rewrite right_id. apply wand_mono; auto.
- rewrite -twp_bind. eapply wand_apply.
{ eapply twp_cas_fail; eauto. by eexists. }
rewrite /= {1}envs_lookup_split //; simpl.
apply sep_mono_r. apply wand_mono; auto.
Qed.
Lemma tac_wp_cas_fail Δ Δ' s E i K l q v e1 v1 e2 Φ :
IntoVal e1 v1 AsVal e2
MaybeIntoLaterNEnvs 1 Δ Δ'
envs_lookup i Δ' = Some (false, l {q} v)%I v v1 vals_cas_compare_safe v v1
envs_lookup i Δ' = Some (false, l {q} v)%I
v v1 vals_cas_compare_safe v v1
envs_entails Δ' (WP fill K (Lit (LitBool false)) @ s; E {{ Φ }})
envs_entails Δ (WP fill K (CAS (Lit (LitLoc l)) e1 e2) @ s; E {{ Φ }}).
Proof.
......@@ -235,7 +274,8 @@ Proof.
Qed.
Lemma tac_twp_cas_fail Δ s E i K l q v e1 v1 e2 Φ :
IntoVal e1 v1 AsVal e2
envs_lookup i Δ = Some (false, l {q} v)%I v v1 vals_cas_compare_safe v v1
envs_lookup i Δ = Some (false, l {q} v)%I
v v1 vals_cas_compare_safe v v1
envs_entails Δ (WP fill K (Lit (LitBool false)) @ s; E [{ Φ }])
envs_entails Δ (WP fill K (CAS (Lit (LitLoc l)) e1 e2) @ s; E [{ Φ }]).
Proof.
......@@ -247,25 +287,29 @@ Qed.
Lemma tac_wp_cas_suc Δ Δ' Δ'' s E i K l v e1 v1 e2 v2 Φ :
IntoVal e1 v1 IntoVal e2 v2
MaybeIntoLaterNEnvs 1 Δ Δ'
envs_lookup i Δ' = Some (false, l v)%I v = v1 vals_cas_compare_safe v v1
envs_lookup i Δ' = Some (false, l v)%I
envs_simple_replace i false (Esnoc Enil i (l v2)) Δ' = Some Δ''
v = v1 val_is_unboxed v
envs_entails Δ'' (WP fill K (Lit (LitBool true)) @ s; E {{ Φ }})
envs_entails Δ (WP fill K (CAS (Lit (LitLoc l)) e1 e2) @ s; E {{ Φ }}).
Proof.
rewrite envs_entails_eq=> ????????; subst.
rewrite -wp_bind. eapply wand_apply; first exact: wp_cas_suc.
rewrite -wp_bind. eapply wand_apply.
{ eapply wp_cas_suc; eauto. by left. }
rewrite into_laterN_env_sound -later_sep envs_simple_replace_sound //; simpl.
rewrite right_id. by apply later_mono, sep_mono_r, wand_mono.
Qed.
Lemma tac_twp_cas_suc Δ Δ' s E i K l v e1 v1 e2 v2 Φ :
IntoVal e1 v1 IntoVal e2 v2
envs_lookup i Δ = Some (false, l v)%I v = v1 vals_cas_compare_safe v v1
envs_lookup i Δ = Some (false, l v)%I
envs_simple_replace i false (Esnoc Enil i (l v2)) Δ = Some Δ'
v = v1 val_is_unboxed v
envs_entails Δ' (WP fill K (Lit (LitBool true)) @ s; E [{ Φ }])
envs_entails Δ (WP fill K (CAS (Lit (LitLoc l)) e1 e2) @ s; E [{ Φ }]).
Proof.
rewrite envs_entails_eq. intros; subst.
rewrite -twp_bind. eapply wand_apply; first exact: twp_cas_suc.
rewrite -twp_bind. eapply wand_apply.
{ eapply twp_cas_suc; eauto. by left. }
rewrite envs_simple_replace_sound //; simpl.
rewrite right_id. by apply sep_mono_r, wand_mono.
Qed.
......@@ -392,6 +436,36 @@ Tactic Notation "wp_store" :=
| _ => fail "wp_store: not a 'wp'"
end.
Tactic Notation "wp_cas" "as" simple_intropattern(H1) "|" simple_intropattern(H2) :=
let solve_mapsto _ :=
let l := match goal with |- _ = Some (_, (?l {_} _)%I) => l end in
iAssumptionCore || fail "wp_cas: cannot find" l "↦ ?" in
iStartProof;
lazymatch goal with
| |- envs_entails _ (wp ?s ?E ?e ?Q) =>
first
[reshape_expr e ltac:(fun K e' =>
eapply (tac_wp_cas _ _ _ _ _ _ K); [iSolveTC|iSolveTC|..])
|fail 1 "wp_cas: cannot find 'CAS' in" e];
[iSolveTC
|solve_mapsto ()
|pm_reflexivity
|try (fast_done || (left; fast_done) || (right; fast_done)) (* vals_cas_compare_safe *)
|intros H1; wp_expr_simpl; try wp_value_head
|intros H2; wp_expr_simpl; try wp_value_head]
| |- envs_entails _ (twp ?E ?e ?Q) =>
first
[reshape_expr e ltac:(fun K e' =>
eapply (tac_twp_cas _ _ _ _ _ K); [iSolveTC|iSolveTC|..])
|fail 1 "wp_cas: cannot find 'CAS' in" e];
[solve_mapsto ()
|pm_reflexivity
|try (fast_done || (left; fast_done) || (right; fast_done)) (* vals_cas_compare_safe *)
|intros H1; wp_expr_simpl; try wp_value_head
|intros H2; wp_expr_simpl; try wp_value_head]
| _ => fail "wp_cas: not a 'wp'"
end.
Tactic Notation "wp_cas_fail" :=
let solve_mapsto _ :=
let l := match goal with |- _ = Some (_, (?l {_} _)%I) => l end in
......@@ -406,7 +480,7 @@ Tactic Notation "wp_cas_fail" :=
[iSolveTC
|solve_mapsto ()
|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]
| |- envs_entails _ (twp ?s ?E ?e ?Q) =>
first
......@@ -415,7 +489,7 @@ Tactic Notation "wp_cas_fail" :=
|fail 1 "wp_cas_fail: cannot find 'CAS' in" e];
[solve_mapsto ()
|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]
| _ => fail "wp_cas_fail: not a 'wp'"
end.
......@@ -433,9 +507,9 @@ Tactic Notation "wp_cas_suc" :=
|fail 1 "wp_cas_suc: cannot find 'CAS' in" e];
[iSolveTC
|solve_mapsto ()
|try congruence
|fast_done || fail "wp_cas_suc: Values are not safe to compare for CAS"
|pm_reflexivity
|try congruence
|try fast_done (* vals_cas_compare_safe *)
|simpl; try wp_value_head]
| |- envs_entails _ (twp ?E ?e ?Q) =>
first
......@@ -443,9 +517,9 @@ Tactic Notation "wp_cas_suc" :=
eapply (tac_twp_cas_suc _ _ _ _ _ K); [iSolveTC|iSolveTC|..])
|fail 1 "wp_cas_suc: cannot find 'CAS' in" e];
[solve_mapsto ()
|try congruence
|fast_done || fail "wp_cas_suc: Values are not safe to compare for CAS"
|pm_reflexivity
|try congruence
|try fast_done (* vals_cas_compare_safe *)
|wp_expr_simpl; try wp_value_head]
| _ => fail "wp_cas_suc: not a 'wp'"
end.
......
......@@ -65,18 +65,27 @@ Proof. apply envs_lookup_sound'. Qed.
Lemma envs_lookup_persistent_sound Δ i P :
envs_lookup i Δ = Some (true,P) of_envs Δ P of_envs Δ.
Proof. intros ?%(envs_lookup_sound' _ false). by destruct Δ. Qed.
Lemma envs_lookup_sound_2 Δ i p P :
envs_wf Δ envs_lookup i Δ = Some (p,P)
?p P of_envs (envs_delete true i p Δ) of_envs Δ.
Proof.
rewrite /envs_lookup /of_envs=>Hwf ?. rewrite [envs_wf Δ⌝%I]pure_True // left_id.
destruct Δ as [Γp Γs], (Γp !! i) eqn:?; simplify_eq/=.
- rewrite (env_lookup_perm Γp) //= intuitionistically_and
and_sep_intuitionistically and_elim_r.
cancel [ P]%I. solve_sep_entails.
- destruct (Γs !! i) eqn:?; simplify_eq/=.
rewrite (env_lookup_perm Γs) //= and_elim_r.
cancel [P]. solve_sep_entails.
Qed.
Lemma envs_lookup_split Δ i p P :
envs_lookup i Δ = Some (p,P) of_envs Δ ?p P (?p P - of_envs Δ).
Proof.
rewrite /envs_lookup /of_envs=>?. apply pure_elim_l=> Hwf.
destruct Δ as [Γp Γs], (Γp !! i) eqn:?; simplify_eq/=.
- rewrite pure_True // left_id (env_lookup_perm Γp) //=
intuitionistically_and and_sep_intuitionistically.
cancel [ P]%I. apply wand_intro_l. solve_sep_entails.
- destruct (Γs !! i) eqn:?; simplify_eq/=.
rewrite (env_lookup_perm Γs) //=. rewrite pure_True // left_id.
cancel [P]. apply wand_intro_l. solve_sep_entails.
intros. apply pure_elim with (envs_wf Δ).
{ rewrite of_envs_eq. apply and_elim_l. }
intros. rewrite {1}envs_lookup_sound//.
apply sep_mono_r. apply wand_intro_l, envs_lookup_sound_2; done.
Qed.
Lemma envs_lookup_delete_sound Δ Δ' rp i p P :
......@@ -198,6 +207,17 @@ Lemma envs_simple_replace_sound Δ Δ' i p P Γ :
of_envs Δ ?p P ((if p then [] Γ else [] Γ) - of_envs Δ').
Proof. intros. by rewrite envs_lookup_sound// envs_simple_replace_sound'//. Qed.
Lemma envs_simple_replace_maybe_sound Δ Δ' i p P Γ :
envs_lookup i Δ = Some (p,P) envs_simple_replace i p Γ Δ = Some Δ'
of_envs Δ ?p P (((if p then [] Γ else [] Γ) - of_envs Δ') (?p P - of_envs Δ)).
Proof.
intros. apply pure_elim with (envs_wf Δ).
{ rewrite of_envs_eq. apply and_elim_l. }
intros. rewrite {1}envs_lookup_sound//. apply sep_mono_r, and_intro.
- rewrite envs_simple_replace_sound'//.
- apply wand_intro_l, envs_lookup_sound_2; done.
Qed.
Lemma envs_simple_replace_singleton_sound Δ Δ' i p P j Q :
envs_lookup i Δ = Some (p,P)
envs_simple_replace i p (Esnoc Enil j Q) Δ = Some Δ'
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment