[Iris-Club] Using Iris

[Gregory Malecha]

Hi, Ralf --

Thanks so much for the pointers. I got a chance to read through a good
chunk of the paper that you pointed me to. I'm sure I'll understand it even
more after I finish a mini-project writing an Iris program logic on top of
Imp, but I, unfortunately, haven't gotten to that yet.

Your responses related to Iris are great and very helpful to me in
understanding the way you guys view things. I have two goals for this
discussion that are slightly tangential to the current discussion, so allow
me to be a bit more clear about them.
1. I am interested in using Iris to build a safety case around concurrent
software. To do this, I need a solid (semi non-technical) explanation for
what Iris means and what it ensures. This motivated my desire to talk about
the overall system invariant which I believe is quite easy to present and
explain. Ideally, I could say that using Iris is just a particular way to
state (and prove) that a property is an inductive invariant of a system.
2. The second thing that I'm wondering about is how I can take properties
proven in Iris and glue them to properties not proved in Iris. For example,
can I use Iris to prove that a piece of C code is "equivalent" to some
functional specification, separately prove something about the functional
specification and then combine the two into an end-to-end theorem that says
that the C code has the high-level property? Ideally, this end-to-end
theorem would only mention the operational semantics of C and the
high-level property, but not "leak" the fact that the proof was performed
using Iris.
Hopefully these goals motivate my desire to look inside the box so to
speak. If I want to establish a property about a system that has one
component verified in Iris, then I need to know how what I proved in Iris
connects to everything else. The paper that you pointed me to has a few
theorems that are useful in understanding this.

On Tue, Oct 30, 2018 at 1:14 PM Ralf Jung <jung at mpi-sws.org> wrote:

> Hi Greg,
>
> I think there are many ways you could do this, and I haven't done the work
> to be
> familiar with the trade-offs.  I am looking forward to reading Robbert's
> paper
> on that. :D
>
I'm looking forward to it as well.

>
> > Thanks, this is helpful in understanding things, I didn't realize this.
> I'll
> > need to look more at the code to better understand how to connect Iris to
> > languages (especially wrt my exploration connecting Iris to C/C++). I
> did some
> > digging into the Language abstractions inside the Iris code base, but
> didn't get
> > a clear enough picture of things.
> >
> > Is this a matter of saying that we have a predicate over ghost states
> (P) and a
> > relation between ghost states and physical states (R), so we can morally
> > construct a predicate over physical states by saying: PP s := exists gs,
> P gs /\
> > R s gs. There's obviously a little bit more going on here from an
> evolution of
> > the system perspective (protocols and the like) but that /might/ just be
> a
> > matter of exposing the existentially quantified ghost state (which you
> almost
> > certainly need to do in the proof).
>
> The iris base logic comes with a notion of "resources" -- "state" if you
> want to
> call it that way.  Being a separation logic, these resourced are treated
> implicitly, i.e. every assertion "P" is just a predicate over resources,
> "P /\ Q" lifts the predicate point-wise, and "P * Q" does what you would
> expect
> from a separation logic.
>
This is what I had expected.

> If we were to compare this with the more traditional terminology you are
> using,
> then these resources are the ghost state: Every Iris assertion says what
> has to
> hold of the ghost state for it to be true.  (Though "truth" is really the
> wrong
> notion here, it's about ownership.)

This makes sense, separation logic is usually described as being about
ownership. Personally, I haven't quite wrapped my head around the
importance of ownership in the presence of things like fictional
separation. I guess we are moving ownership from "locations" (the way they
are in classical CSL) to "permissions" (which are akin to actions in a
protocol)?

Returning to my high-level motivations, we use ownership of a thread to
ensure that other threads don't break our thread's invariant when they run.
Concretely, with the program P1 || P2 then the invariant about the full
system (I) is actually built from the (classical) conjunction of two
invariants I1 and I2 which are invariants of P1 and P2 respectively. At the
highest level, we have to prove that P1 and P2 both preserve both I1 and
I2. Our local proofs only establish that P1 preserves I1 and P2 preserves
I2, we need the underlying logic to establish the other preservation "for
free" (in the soundness proof of the program logic, in Iris, I imagine,
this proof is handled completely within the base logic). Getting things
"for free" is, after all, the reason that we pursue new logics :-). In the
original CSL work, this "free theorem" (different than, but related to, the
usual use of "theorems for free") is achieve through true separation, and
the CSL soundness proof would use this separation to establish the fact
that I1 is maintained by any modifications to P2's private state.
Rely-Guarantee, in my mind, refines this notion by saying that both can
talk about the same state, as long as they agree on how the other modifies
any overlapping state, exactly as above, P1 relies on P2 not modifying any
of its private memory. For shared memory, the rely-guarantee specifies a
protocol that both accept.

  But since we build our program logic
> *inside* the base logic, we don't think of these assertions as predicates
> over
> some state; we think of them as propositions that can implicitly claim
> ownership.

Is it accurate to think of "ownership" as "permissions to do something" or
is there some difference between them?

I have been thinking of Iris as "very fine grained permissions" in a sort
of rely-guarantee/protocol-style, essentially saying that separation is
just a degenerate sort of protocol where only one participant is allowed to
do anything. By solving this problem in full generality (at the level of
protocols), then you can have much more interesting protocols which is one
the main bits about Iris (from the original Iris versions and GPS).
In addition (and complementary) to fine-grained permissions, the other Iris
insight is the fact that protocols can themselves be hidden, so I don't
need to expose the protocols to my state to clients as long as I
encapsulate my state appropriately. Perhaps this is another aspect of the
ownership that you're thinking about.

>   In particular, even the adequacy proof of WP does not ever talk
> about "ghost state", it is entirely performed inside the Iris base logic
> (so
> resources are implicit), and ultimately defers to the soundness theorem of
> the
> base logic itself.

I'll need to look a the paper you pointed me to.

>

The definition of WP involves a "state interpretation", which is a predicate
> over physical state -- but it is a predicate *in Iris* (PState -> iProp),
> so
> really it is a relation between physical and ghost state because iProp is
> itself
> a predicate (if you choose to unfold the Iris model, which I do not think
> is the
> best way to think about this).  The state interpretation is used to
> connect the
> ghost state to the physical state -- one way to think about this is to let
> the
> state interpretation say "that part of the ghost state is owned by us, and
> it is
> equal to the physical state".  But it could be anything.  The key point is
> that
> because our ghost state is flexible enough to encode all sorts of sharing,
> we
> can entirely define \mapsto and friends in ghost state, and use the state
> interpretation to make all of that "mean anything".  It's a bit like in
> "Fictional Separation Logic" (Jensen, Birkedal), except that *all*
> separation is
> fiction in Iris (and so none is, you could say ;).
>
> I suggest reading the Iris 3 paper
> <https://iris-project.org/pdfs/2017-esop-iris3-final.pdf>, it develops a
> definition of WP and \mapsto inside the base logic step-by-step; that
> should
> help explain how we set these things up.  If you want, I'd also be happy
> to chat
> about this and interactively answer the questions that will likely come
> up. :)
>
> Kind regards,
> Ralf



-- 
gregory malecha
gmalecha.github.io
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.mpi-sws.org/pipermail/iris-club/attachments/20181105/3fa660ea/attachment.html>