• Robbert Krebbers's avatar
    Fine-grained post-conditions for forked-off threads. · ebf06f91
    Robbert Krebbers authored
    This commit extends the state interpretation with an additional parameter to
    talk about the number of forked-off threads, and a fixed postcondition for each
    forked-off thread:
    
        state_interp : Λstate → list Λobservation → nat → iProp Σ;
        fork_post : iProp Σ;
    
    This way, instead of having `True` as the post-condition of `Fork`, one can
    have any post-condition, which is then recorded in the state interpretation.
    The point of keeping track of the postconditions of forked-off 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 post-conditions
    `[∗] replicate m fork_post` of all forked-off 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 fork-based concurrency.
    ebf06f91
Name
Last commit
Last update
benchmark Loading commit data...
docs Loading commit data...
tests Loading commit data...
theories Loading commit data...
.gitattributes Loading commit data...
.gitignore Loading commit data...
.gitlab-ci.yml Loading commit data...
.gitmodules Loading commit data...
CHANGELOG.md Loading commit data...
CONTRIBUTING.md Loading commit data...
Editor.md Loading commit data...
LICENSE Loading commit data...
LICENSE-CODE Loading commit data...
LICENSE-DOCS Loading commit data...
Makefile Loading commit data...
Makefile.coq.local Loading commit data...
Naming.md Loading commit data...
ProofMode.md Loading commit data...
README.md Loading commit data...
_CoqProject Loading commit data...
awk.Makefile Loading commit data...
descr Loading commit data...
opam Loading commit data...