Skip to content

GitLab

  • Projects
  • Groups
  • Snippets
  • Help
    • Loading...
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
    • Contribute to GitLab
  • Sign in / Register
I
Iris
  • Project overview
    • Project overview
    • Details
    • Activity
    • Releases
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
  • Issues 122
    • Issues 122
    • List
    • Boards
    • Labels
    • Service Desk
    • Milestones
  • Merge Requests 18
    • Merge Requests 18
  • CI / CD
    • CI / CD
    • Pipelines
    • Jobs
    • Schedules
  • Operations
    • Operations
    • Incidents
    • Environments
  • Analytics
    • Analytics
    • CI / CD
    • Repository
    • Value Stream
  • Wiki
    • Wiki
  • Members
    • Members
  • Activity
  • Graph
  • Create a new issue
  • Jobs
  • Commits
  • Issue Boards
Collapse sidebar
  • Iris
  • Iris
  • Merge Requests
  • !614

Merged
Opened Jan 05, 2021 by Robbert Krebbers@robbertkrebbersMaintainer

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

  • Overview 10
  • Commits 5
  • 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
Reviewer
Request review from
None
Milestone
None
Assign milestone
Time tracking
Reference: iris/iris!614
Source branch: robbert/iMod_iInv_atomic