Skip to content
GitLab
Projects Groups Snippets
  • /
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
    • Contribute to GitLab
  • Sign in / Register
  • Iris Iris
  • Project information
    • Project information
    • Activity
    • Labels
    • Members
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
  • Issues 171
    • Issues 171
    • List
    • Boards
    • Service Desk
    • Milestones
  • Merge requests 15
    • Merge requests 15
  • CI/CD
    • CI/CD
    • Pipelines
    • Jobs
    • Schedules
  • Deployments
    • Deployments
    • Releases
  • Analytics
    • Analytics
    • Value stream
    • CI/CD
    • Repository
  • Wiki
    • Wiki
  • Activity
  • Graph
  • Create a new issue
  • Jobs
  • Commits
  • Issue Boards
Collapse sidebar
  • Iris
  • IrisIris
  • Merge requests
  • !614

Better errors when opening an invariant/mask changing update around a non-atomic WP

  • Review changes

  • Download
  • Email patches
  • Plain diff
Merged Robbert Krebbers requested to merge robbert/iMod_iInv_atomic into master Jan 05, 2021
  • Overview 10
  • Commits 5
  • Pipelines 0
  • Changes 11

This MR ensures that opening an invariant or eliminating a mask-changing update modality around a non-atomic weakest precondition creates an side-condition Atomic .... Before, this would fail with the mysterious error "iMod: cannot eliminate modality (|={E1,E2}=> ...) in (WP ...)".

For example:

Lemma wp_iInv_atomic_acc N E P :
  ↑ N ⊆ E →
  inv N P -∗ WP #() #() @ E {{ _, True }}.
Proof.
  iIntros (?) "H". iInv "H" as "H".
Abort.

This now creates a side-condition Atomic (stuckness_to_atomicity NotStuck) (#() #()).

The new behavior is implemented by threading the side-condition Atomic through the instances for ElimModal, ElimInv, and ElimAcc. This makes sure that the side-condition is not established during TC search, but afterwards. For example:

   Global Instance elim_modal_fupd_wp_atomic p s E1 E2 e P Φ :
-    Atomic (stuckness_to_atomicity s) e →
-    ElimModal True p false (|={E1,E2}=> P) P
-            (WP e @ s; E1 {{ Φ }}) (WP e @ s; E2 {{ v, |={E2,E1}=> Φ v }})%I.
+    ElimModal (Atomic (stuckness_to_atomicity s) e) p false
+            (|={E1,E2}=> P) P
+            (WP e @ s; E1 {{ Φ }}) (WP e @ s; E2 {{ v, |={E2,E1}=> Φ v }})%I | 100.

A parameter for such a side-condition was already present in the ElimModal and ElimInv classes, but this MR also adds it to the ElimAcc class.

Edited Jan 05, 2021 by Robbert Krebbers
Assignee
Assign to
Reviewers
Request review from
Time tracking
Source branch: robbert/iMod_iInv_atomic