<div dir="ltr"><div>Hi, Ralf --</div><div><br></div>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. <div><br></div><div>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.</div><div>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.</div><div>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.</div><div>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.</div><div><br><div class="gmail_quote"><div dir="ltr">On Tue, Oct 30, 2018 at 1:14 PM Ralf Jung <<a href="mailto:jung@mpi-sws.org" target="_blank">jung@mpi-sws.org</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Hi Greg,<br>
<br>
I think there are many ways you could do this, and I haven't done the work to be<br>
familiar with the trade-offs.  I am looking forward to reading Robbert's paper<br>
on that. :D<br></blockquote><div>I'm looking forward to it as well. </div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
<br>
> Thanks, this is helpful in understanding things, I didn't realize this.  I'll<br>
> need to look more at the code to better understand how to connect Iris to<br>
> languages (especially wrt my exploration connecting Iris to C/C++). I did some<br>
> digging into the Language abstractions inside the Iris code base, but didn't get<br>
> a clear enough picture of things.<br>
> <br>
> Is this a matter of saying that we have a predicate over ghost states (P) and a<br>
> relation between ghost states and physical states (R), so we can morally<br>
> construct a predicate over physical states by saying: PP s := exists gs, P gs /\<br>
> R s gs. There's obviously a little bit more going on here from an evolution of<br>
> the system perspective (protocols and the like) but that /might/ just be a<br>
> matter of exposing the existentially quantified ghost state (which you almost<br>
> certainly need to do in the proof).<br>
<br>
The iris base logic comes with a notion of "resources" -- "state" if you want to<br>
call it that way.  Being a separation logic, these resourced are treated<br>
implicitly, i.e. every assertion "P" is just a predicate over resources,<br>
"P /\ Q" lifts the predicate point-wise, and "P * Q" does what you would expect<br>
from a separation logic.<br></blockquote><div>This is what I had expected. </div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
If we were to compare this with the more traditional terminology you are using,<br>
then these resources are the ghost state: Every Iris assertion says what has to<br>
hold of the ghost state for it to be true.  (Though "truth" is really the wrong<br>
notion here, it's about ownership.)</blockquote><div>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)?</div><div><br></div><div>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<i> </i>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.</div><div><br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">  But since we build our program logic<br>
*inside* the base logic, we don't think of these assertions as predicates over<br>
some state; we think of them as propositions that can implicitly claim<br>
ownership.</blockquote><div>Is it accurate to think of "ownership" as "permissions to do something" or is there some difference between them? </div><div><br></div><div>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).</div><div>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.<br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">  In particular, even the adequacy proof of WP does not ever talk<br>
about "ghost state", it is entirely performed inside the Iris base logic (so<br>
resources are implicit), and ultimately defers to the soundness theorem of the<br>
base logic itself.</blockquote><div>I'll need to look a the paper you pointed me to. </div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"> </blockquote><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
The definition of WP involves a "state interpretation", which is a predicate<br>
over physical state -- but it is a predicate *in Iris* (PState -> iProp), so<br>
really it is a relation between physical and ghost state because iProp is itself<br>
a predicate (if you choose to unfold the Iris model, which I do not think is the<br>
best way to think about this).  The state interpretation is used to connect the<br>
ghost state to the physical state -- one way to think about this is to let the<br>
state interpretation say "that part of the ghost state is owned by us, and it is<br>
equal to the physical state".  But it could be anything.  The key point is that<br>
because our ghost state is flexible enough to encode all sorts of sharing, we<br>
can entirely define \mapsto and friends in ghost state, and use the state<br>
interpretation to make all of that "mean anything".  It's a bit like in<br>
"Fictional Separation Logic" (Jensen, Birkedal), except that *all* separation is<br>
fiction in Iris (and so none is, you could say ;).<br>
<br>
I suggest reading the Iris 3 paper<br>
<<a href="https://iris-project.org/pdfs/2017-esop-iris3-final.pdf" rel="noreferrer" target="_blank">https://iris-project.org/pdfs/2017-esop-iris3-final.pdf</a>>, it develops a<br>
definition of WP and \mapsto inside the base logic step-by-step; that should<br>
help explain how we set these things up.  If you want, I'd also be happy to chat<br>
about this and interactively answer the questions that will likely come up. :)<br>
<br>
Kind regards,<br>
Ralf</blockquote></div><br clear="all"><div><br></div>-- <br><div dir="ltr" class="m_-3575626812065642987gmail_signature" data-smartmail="gmail_signature"><div dir="ltr"><div><div dir="ltr"><div>gregory malecha</div><div><a href="https://gmalecha.github.io" target="_blank">gmalecha.github.io</a></div></div></div></div></div></div></div>