...
 
Commits (2)
......@@ -26,10 +26,15 @@ variables:
## Build jobs
build-coq.8.8.0:
build-coq.8.9.0:
<<: *template
variables:
OPAM_PINS: "coq version 8.8.0"
OPAM_PINS: "coq version 8.9.0"
build-coq.8.8.2:
<<: *template
variables:
OPAM_PINS: "coq version 8.8.2"
build-coq.8.7.2:
<<: *template
......
......@@ -54,6 +54,8 @@ accesses. In the current semantics, we treat racing between `plain`
accesses as UB, so as to model non-atomics. We implement a race detector similar
to the one in [iGPS][iGPS].
#### TODO: the race detector is unsound!
Note that there's a difference in the race detector between non-atomic reads
and other operations.
......@@ -94,7 +96,7 @@ To find all the dependencies of ra-gps, opam needs to know about the Coq and Iri
opam archives. This can be achieved by executing
```
opam repo add coq-released https://coq.inria.fr/opam/released
opam repo add iris-dev https://gitlab.mpi-sws.org/FP/opam-dev.git
opam repo add iris-dev https://gitlab.mpi-sws.org/iris/opam.git
```
Now, execute `make build-dep` to install all dependencies.
......@@ -104,4 +106,4 @@ Finally, execute `make` to build the development.
[promising]: http://sf.snu.ac.kr/promise-concurrency/
[iGPS]: https://gitlab.mpi-sws.org/FP/sra-gps
[stdpp]: https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp
[stdpp]: https://gitlab.mpi-sws.org/iris/stdpp
......@@ -9,6 +9,6 @@ build: [make "-j%{jobs}%"]
install: [make "install"]
remove: ["rm" "-rf" "%{lib}%/coq/user-contrib/promising"]
depends: [
"coq" { (>= "8.7.0" & < "8.9~") | (= "dev") }
"coq-stdpp" { (= "dev.2018-07-23.1.4fb641ed") | (= "dev") }
"coq" { (>= "8.7.0" & < "8.10~") | (= "dev") }
"coq-stdpp" { (= "dev.2019-01-29.2.cbb67c16") | (= "dev") }
]
......@@ -87,7 +87,6 @@ Section Memory.
by do 2 case: (_!!t)=>[?|]; inversion 1.
Qed.
Lemma cell_le_non_empty (C1 C2: cell) (LE: cell_le C1 C2): C1 C2 .
Proof.
split => NE;
......@@ -2105,7 +2104,7 @@ Section Memory.
{ rewrite -HL1 -{2}(Eqm n1)-lookup_app_r; [auto|simpl; omega]. }
have HL2': (𝑚 :: 𝑚s) !! (n2 + 1)%nat = Some 𝑚2.
{ rewrite -HL2 -{2}(Eqm n2)-lookup_app_r; [auto|simpl; omega]. }
assert (EQ := DISJ _ _ _ _ HL1' HL2' Eq). by omega.
assert (EQ := DISJ _ _ _ _ HL1' HL2' Eq). by lia.
Qed.
Lemma mem_list_disj_cons_rest 𝑚 𝑚s :
......@@ -2114,9 +2113,9 @@ Section Memory.
move => DISJ 𝑚' /elem_of_list_lookup [i HL2] Eq.
have HL1: (𝑚 :: 𝑚s) !! 0%nat = Some 𝑚 by auto.
have HL2': (𝑚 :: 𝑚s) !! (i + 1)%nat = Some 𝑚'.
{ rewrite (lookup_app_r [𝑚]); simpl; last by omega.
rewrite (_: (i + 1 - 1)%nat = i); by [auto|omega]. }
have ?:=DISJ _ _ _ _ HL1 HL2' Eq. by omega.
{ rewrite (lookup_app_r [𝑚]); simpl; last by lia.
rewrite (_: (i + 1 - 1)%nat = i); by [auto|lia]. }
have ?:=DISJ _ _ _ _ HL1 HL2' Eq. by lia.
Qed.
Lemma mem_list_addins_old 𝑚s M1 M2 l
......@@ -2560,14 +2559,14 @@ Section Memory.
(n' < n)%nat
(cell_list' l n M Cl) !! n' = Some C M !!c (l >> n') = C.
Proof.
induction n as [|n IH] => n' C Cl HCl Lt; first by omega.
induction n as [|n IH] => n' C Cl HCl Lt; first by lia.
simpl. apply lt_n_Sm_le, le_lt_or_eq in Lt as [Lt|Eq].
- apply IH; [|done] => n0 C0.
rewrite /cell_cons. destruct n0 as [|n0].
+ move => /= [<-]. by rewrite -plus_n_O.
+ rewrite (lookup_app_r [_] Cl); last by (simpl; omega).
+ rewrite (lookup_app_r [_] Cl); last by (simpl; lia).
move => /= /HCl. rewrite -minus_n_O.
rewrite (_: (S n + n0)%nat = (n + S n0)%nat); [done|omega].
rewrite (_: (S n + n0)%nat = (n + S n0)%nat); [done|lia].
- rewrite Eq cell_list'_lookup; last done.
rewrite Nat.sub_diag /cell_cons /=. split; congruence.
Qed.
......@@ -2586,7 +2585,7 @@ Section Memory.
Proof.
move => n' C In. apply (cell_list_Some _ n); last done.
apply lookup_lt_Some in In.
rewrite cell_list'_length_exact /= in In. by omega.
rewrite cell_list'_length_exact /= in In. by lia.
Qed.
Lemma cell_list_fmap (l : loc) (n: nat) (M: memory) :
......@@ -2655,7 +2654,7 @@ Section Memory.
Lemma cell_cut_insert C t t' m :
(t t')%Qc
cell_cut t (<[t' := m]> C) = <[t' := m]> (cell_cut t C).
Proof. move=>?. by rewrite /cell_cut map_filter_lookup_insert. Qed.
Proof. move=>?. by rewrite /cell_cut -map_filter_insert. Qed.
Lemma cell_cut_empty C t
(MAX: t', is_Some (C !! t') t' < t) :
......
......@@ -741,12 +741,12 @@ Section AllocSteps.
have MA : mem_list_addins (alloc_messages n (l >> 1)) M1
(alloc_new_mem M1 (alloc_messages n (l >> 1))).
{ apply (IH (l >> 1)).
move => n' Lt. rewrite (shift_nat_assoc _ 1). apply FRESH. by omega. }
move => n' Lt. rewrite (shift_nat_assoc _ 1). apply FRESH. by lia. }
econstructor; [exact MA| |by constructor|done].
econstructor. simpl.
rewrite -(mem_list_addins_old _ _ _ _ MA).
* rewrite (_ : _ !!c _ = ); first done.
apply memory_loc_not_elem_of_dom, (FRESH 0). by omega.
apply memory_loc_not_elem_of_dom, (FRESH 0). by lia.
* apply alloc_messages_shift_1.
Qed.
......@@ -765,13 +765,13 @@ Section AllocSteps.
set 𝓥' := alloc_new_tview (alloc_messages n (l >> 1)) 𝓥1.
have MA : alloc_helper (alloc_messages n (l >> 1)) 𝓥1 𝓥'.
{ apply (IH (l >> 1)).
move => n' Lt. rewrite (shift_nat_assoc _ 1). apply FRESH. by omega. }
move => n' Lt. rewrite (shift_nat_assoc _ 1). apply FRESH. by lia. }
clear IH.
have HRlx : rlx (cur 𝓥') !! (l >> 0) = None. {
rewrite -(alloc_helper_cur_old _ _ _ _ MA);
last by apply alloc_messages_shift_1.
apply (closed_timenap_memory_None _ M1); last apply HC.
apply memory_loc_not_elem_of_dom, (FRESH 0). by omega. }
apply memory_loc_not_elem_of_dom, (FRESH 0). by lia. }
have HRel : rel 𝓥' !! (l >> 0) = None.
{ rewrite -(alloc_helper_rel_old _ _ _ _ MA);
last by apply alloc_messages_shift_1.
......@@ -779,7 +779,7 @@ Section AllocSteps.
destruct (closed_view_rlx _ _ (closed_tview_cur _ _ HC) _ _
(timeNap_lookup_w _ _ _ _ _ Eq))
as [m [t' [_ Eqm]]].
apply (FRESH 0); first by omega. rewrite memory_lookup_cell in Eqm.
apply (FRESH 0); first by lia. rewrite memory_lookup_cell in Eqm.
apply memory_loc_elem_of_dom=>EQ. by rewrite EQ in Eqm. }
econstructor; [exact MA|]. simpl.
erewrite ->threadView_eq; [econstructor|..]=>//=.
......@@ -919,12 +919,12 @@ Section AllocSteps.
(dealloc_new_mem M (dealloc_messages M n (l >> 1))).
{ apply (IH (l >> 1));
[move => ??|move => ??]; rewrite (shift_nat_assoc _ 1);
[apply NEMP|apply REMOVE]; by omega. } clear IH.
[apply NEMP|apply REMOVE]; by lia. } clear IH.
rewrite /𝑚s dealloc_messages_cons.
econstructor; [exact MA|..].
+ assert ( t0 m0, cell_max (M !!c (l >> 0)) = Some (t0, m0)) as [t0 [m0 Eqm0]].
{ apply gmap_top_nonempty; eauto with typeclass_instances.
by apply (NEMP 0); omega. }
by apply (NEMP 0); lia. }
have HL: M !!c (l >> 0)
= dealloc_new_mem M (dealloc_messages M n (l >> 1)) !!c (l >> 0).
{ rewrite (mem_list_addins_old _ _ _ _ MA); first done.
......@@ -952,7 +952,7 @@ Section AllocSteps.
set 𝓥' := dealloc_new_tview (dealloc_messages M1 n (l >> 1)) 𝓥1.
have MA : alloc_helper (dealloc_messages M1 n (l >> 1)) 𝓥1 𝓥'.
{ apply (IH (l >> 1)) => n' Lt. rewrite (shift_nat_assoc _ 1).
apply REMOVE. by omega. } clear IH.
apply REMOVE. by lia. } clear IH.
econstructor; [exact MA|].
econstructor=>//. remember (mloc _) as l'.
rewrite -(_: rlx (cur 𝓥1) !!w l' = rlx (cur 𝓥') !!w l'); last first.
......