 22 Mar, 2019 1 commit


Rodolphe Lepigre authored

 19 Mar, 2019 2 commits


Rodolphe Lepigre authored

Rodolphe Lepigre authored

 14 Mar, 2019 1 commit


Robbert Krebbers authored

 05 Mar, 2019 1 commit


Ralf Jung authored

 29 Nov, 2018 1 commit


Tej Chajed authored
Adding a hint without a database now triggers a deprecation warning in Coq master (https://github.com/coq/coq/pull/8987).

 31 Oct, 2018 4 commits


Robbert Krebbers authored

Robbert Krebbers authored

Robbert Krebbers authored
This commit extends the state interpretation with an additional parameter to talk about the number of forkedoff threads, and a fixed postcondition for each forkedoff thread: state_interp : Λstate → list Λobservation → nat → iProp Σ; fork_post : iProp Σ; This way, instead of having `True` as the postcondition of `Fork`, one can have any postcondition, which is then recorded in the state interpretation. The point of keeping track of the postconditions of forkedoff threads, is that we get an (additional) stronger adequacy theorem: Theorem wp_strong_all_adequacy Σ Λ `{invPreG Σ} s e σ1 v vs σ2 φ : (∀ `{Hinv : invG Σ} κs, (={⊤}=> ∃ (stateI : state Λ → list (observation Λ) → nat → iProp Σ) (fork_post : iProp Σ), let _ : irisG Λ Σ := IrisG _ _ _ Hinv stateI fork_post in stateI σ1 κs 0 ∗ WP e @ s; ⊤ {{ v, let m := length vs in stateI σ2 [] m ∗ [∗] replicate m fork_post ={⊤,∅}=∗ ⌜ φ v ⌝ }})%I) → rtc erased_step ([e], σ1) (of_val <$> v :: vs, σ2) → φ v. The difference with the ordinary adequacy theorem is that this one only applies once all threads terminated. In this case, one gets back the postconditions `[∗] replicate m fork_post` of all forkedoff threads. In Iron we showed that we can use this mechanism to make sure that all resources are disposed of properly in the presence of forkbased concurrency.

JacquesHenri Jourdan authored

 29 Oct, 2018 3 commits


JacquesHenri Jourdan authored

Robbert Krebbers authored
Other heap_lang related instances in that file too. Now, the tactics file only contains stuff related to actual tactics.

JacquesHenri Jourdan authored
We add a specific constructor to the type of expressions for injecting values in expressions. The advantage are :  Values can be assumed to be always closed when performing substitutions (even though they could contain free variables, but it turns out it does not cause any problem in the proofs in practice). This means that we no longer need the `Closed` typeclass and everything that comes with it (all the reflectionbased machinery contained in tactics.v is no longer necessary). I have not measured anything, but I guess this would have a significant performance impact.  There is only one constructor for values. As a result, the AsVal and IntoVal typeclasses are no longer necessary: an expression which is a value will always unify with `Val _`, and therefore lemmas can be stated using this constructor. Of course, this means that there are two ways of writing such a thing as "The pair of integers 1 and 2": Either by using the value constructor applied to the pair represented as a value, or by using the expression pair constructor. So we add reduction rules that transform reduced pair, injection and closure expressions into values. At first, this seems weird, because of the redundancy. But in fact, this has some meaning, since the machine migth actually be doing something to e.g., allocate the pair or the closure. These additional steps of computation show up in the proofs, and some additional wp_* tactics need to be called.

 18 Oct, 2018 4 commits
 05 Oct, 2018 7 commits


Robbert Krebbers authored

Ralf Jung authored

Ralf Jung authored

Ralf Jung authored

Marianna Rapoport authored

Marianna Rapoport authored
 Removing head of list of observations after each reduction step in definition of wp  Adding support for observations to state_interp and world  Applying Ralf's suggestions to previous commit (e.g. replacing /\ and > with unicode characters)

Marianna Rapoport authored

 04 Oct, 2018 1 commit


Ralf Jung authored

 28 Jun, 2018 1 commit


Ralf Jung authored
This restricts CAS to only be able to compare literals with literals, NONEV with NONEV and NONEV with SOMEV for a literal.

 18 Jun, 2018 2 commits
 18 May, 2018 1 commit


Robbert Krebbers authored

 03 Mar, 2018 1 commit


Robbert Krebbers authored

 13 Jan, 2018 1 commit


Robbert Krebbers authored

 07 Dec, 2017 1 commit


Ralf Jung authored

 05 Dec, 2017 1 commit


Robbert Krebbers authored

 23 Nov, 2017 1 commit


Robbert Krebbers authored

 09 Nov, 2017 4 commits


David Swasey authored
This reverts commit 913059d2.

David Swasey authored
I saw no need for `stuckness_flip`: strong atomicity always works, while weak atomicity works only for expressions that are not stuck. Since this seemed unclear, I split lemma `wp_atomic'` up into `wp_strong_atomic` (parametric in the WP's `s`) and `wp_weak_atomic` (not). The proof mode instance is stated in terms of the derived rule `wp_atomic` (parametric in `s`).

David Swasey authored

 08 Nov, 2017 2 commits


David Swasey authored

David Swasey authored
