Skip to content

GitLab

  • Menu
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 148
    • Issues 148
    • List
    • Boards
    • Service Desk
    • Milestones
  • Merge requests 9
    • Merge requests 9
  • CI/CD
    • CI/CD
    • Pipelines
    • Jobs
    • Schedules
  • Deployments
    • Deployments
    • Environments
    • Releases
  • Monitor
    • Monitor
    • Incidents
  • Analytics
    • Analytics
    • Value stream
    • CI/CD
    • Repository
  • Wiki
    • Wiki
  • Activity
  • Graph
  • Create a new issue
  • Jobs
  • Commits
  • Issue Boards
Collapse sidebar
  • Iris
  • IrisIris
  • Issues
  • #12

Closed
Open
Created Jan 06, 2016 by Ralf Jung@jungOwner

Prove stronger stepping frame rule

Right now, we have a "stepping frame rule" that looks as follows:

{ P } e { Q }    e is not a value
------------------------------------
{ \later R * P } e { R * Q }

Essentially, this allows us to step away a later when framing around any non-value. (We also sometimes call this the "atomic frame rule", since atomic expressions are never values. But the one above is just as valid, and obviously stronger.)

However, I think I will need for my Rust stuff a stronger version of this rule, that allows me to strip away a later inside an invariant from any non-value. This comes up because I have non-atomic reads and writes that are, well, non-atomic, and I still want to strip away a later from something that is located inside an invariant[1]. This rule is rather awkward to write down in terms of Hoare triples and view shifts:

R0 E1^==>^E2 \later R1    R1 E2^==>^E1 R2    { P } e { Q }_E1
   e is not a value     E2 <= E1
------------------------------------------------------------------
{ R0 * P } e { R2 * Q }_E1

It looks nicer in terms of primitive view shifts and weakest-pre:

wp_E1 e Q * vs_E1^E2(\later vs_E2^E1(R))
   e is not a value     E2 <= E1
-------------------------------------
   wp_E1 e (Q * R)

When we re-do the weakest-pre proofs for V2.0, I think this is the rule we should show. (And derive the old one, of course.)

[1] If you are curious: The invariant has two states "vs(P)" and "P", with an STS making sure that one can only go from the 1st state to the 2nd. The rule I need allows me to open this invariant alongside the non-atomic access, obtain "\later (vs(P) / P)", strip away the later, view shift to "P", and put that back into the invariant; taking out the witness that the view shift has been performed. I do not need any resource from the invariant to justify the memory access, so it's fine for that one to be non-atomic. But I do need to perform this view shift, because immediately after the access I will want to open the invariant again and know I get "\later P", without any more skips.

Cc: @robbertkrebbers @swasey @janno

Assignee
Assign to
Time tracking