[Iris-Club] Using Iris

[Gregory Malecha]

Hi, Ralf --

On Mon, Oct 15, 2018, 6:45 AM Ralf Jung <jung at mpi-sws.org> wrote:

> Hi Greg,
>
> > This is an interesting conversation, I'm learning a lot, so thanks.
>
> So am I. :)
>
> >     Ah, that is an interesting approach.  In our case we re-used the
> same definition
> >     of WP and Hoare triples as "normal" (non-CPS) languages, so we
> likely wouldn't
> >     want to derive all the WP laws for this tweaked WP that incorporates
> an
> >     "off" state.
> >
> > This particular solution of introducing the "on-off" state is useful for
> the
> > entire system, but it might be solving too restricted of a problem to
> make
> > things clear. Suppose we are trying to implement a threading library that
> > exposes "thread_exit" which stops running our thread. We wouldn't want
> to add a
> > state to our system to capture "this thread has ended". At the high
> level, we
> > would formalize threads the way you do in heap_lang, but at the
> implementation
> > level, we would need to make sure that the thread entry point doesn't pop
> > anything off the stack because it is the first thing on the stack.
> Rather, it
> > needs to call (probably just a jump to) the "thread_exit" function so
> that it
> > can schedule the next thing. In both cases, a False post-condition (from
> the
> > client point of view) seems appropriate.
>
> I am not sure I am entirely following.  I think we would want to add a
> state to
> our system saying "this thread has ended"; somehow the high-level
> specification
> has to reflect what happens in that case, doesn't it?
>
Yes. This could would likely be reflected in the implementation by freeing
the resources associated with the thread, e.g. the TCB. If False was the
postcondition of the thread, then the thread library would have to actually
remove it from the system so that False doesn't show up in the invariant.

>
> >     I could imagine a slightly different take on this though (that also
> feels more
> >     "Irisy" to me): Say we add that state, and we also add a new
> separation logic
> >     assertion you can make about the state saying that it is off. (This
> would be
> >     duplicable because once off, it is off forever.) Then we could make
> the
> >     postcondition of the `halt` continuation say "the machine is off",
> and also use
> >     that as the universal postcondition everywhere. This would only
> require very
> >     local changes to LambdaRust.
> >
> > This is reasonable for whole-program termination, though it might be the
> case
> > that folding it into the system actually makes more sense. It might also
> be that
> > you could just define terminal states appropriately in your system and
> you
> > wouldn't need to change anything.
>
> Currently a terminal state is a value.  I am not sure if adding "any
> expression
> having HALT at evaluation position" as a value would work out so well.
>
Also, the postcondition of WP is a predicate over the terminal state, so
> making
> "K[HALT]" one of those would still mean we need special treatment that
> makes
> this a different kind of terminal state than the rest of them.
>
These are interesting points. I'm wondering how much this is an artifact of
heap_lang/lambdaRust rather than the Iris logic. If I were to encode C, a
la CompCert, then I'd have commands that return in one of 4 ways, normal
termination, return, break, and continue, would the current formulation of
WP be good for that? You can always use the continuation pointer encoding
(discussed below), but in that case it doesn't even need the value in the
post-condition, though you still need it for doing expressions. Perhaps we
could just say that commands always return unit?

>
> >     I should probably write this down in case we want to change our
> story there.^^
> >     It seems slightly annoying to have to say in every reduction step
> that also the
> >     global "has the machine halted" flag is not set yet, but that's a
> one-time pain
> >     so it's probably not too bad.  (This would likely be easier with a
> different
> >     setup, but the shared Iris definition of WP assumes that there is a
> pool of
> >     threads which all carry some per-thread state [for us, that's the
> expression,
> >     the code still to be run there -- because we are using substitution,
> there are
> >     no environments] and then some global state [the heap, usually].
> Halting is a
> >     clearly a cross-thread concern, but we only define a per-thread
> reduction which
> >     is the automatically lifted to a thread pool.  So we would add a
> flag in the
> >     global state to reflect whether the machine has halted, and not
> allow any
> >     further per-thread reductions after that happened.  We could of
> course also
> >     decide not to use the shared WP, define our own, and still benefit
> from most of
> >     the Iris machinery [the proof mode and invariants and all that would
> still just
> >     work], but we usually try to avoid that.)
> >
> > Just to throw one other thing on the table about code-pointers and Hoare
> > doubles. I like the uniformity that code-pointers provide for control
> flow
> > operators in languages such as C. For example, VST has 4 possible
> > post-conditions (normal termination, doing a 'return', doing a 'break',
> and
> > doing a 'continue'). If you reflect all these simply as function
> pointers, then
> > you don't need any fundamental support in your logic for this sort of
> > multiple-return types.
>
> Yeah, that's one reason we used lambda-terms for this in lambdaRust: If we
> ever
> want to add support for `panic!` (which Rust's form of unwinding, like C++
> exceptions), then that'd just be another continuation.  It wouldn't be
> special
> in the operational semantics at all.
>
Continuations are great! :-)

>
> > When I say "invariant" here, I am thinking of the base definition of
> invariant
> > without any nice reasoning principles on top of it. For example, for any
> system
> > described by (s0, step), you have s is an invariant (I) if `forall s,
> step^* s0
> > s -> I s`. From the thread-local invariants (which are dependent on the
> > permissions of each thread and the pc of the thread) we construct I by
> saying
> > something like "the assertions of all threads can be starred together".
> While I
> > don't have the deepest understanding of how Iris invariants work, I
> would assume
> > that they fit into this somehow, otherwise WP would be difficult to
> prove sound.
>
> Ah, so that would be the induction hypothesis maintained by the WP
> soundness
> proof.

The setup is slightly different because WP is a separation logic
> assertion that can own something. Basically, if the current program state
> is


>   ([e_0, ..., e_n], \sigma)  ( thread pool of expressions, and shared
> state )
>
> and the final postcondition is Q, then the invariant is the following
> separation
> logic assertion (we are doing this induction, the WP soundness proof,
> inside Iris):
>
>   world \sigma * WP e_0 {{ Q }} * WP e_1 {{ True }} * ... * WP e_n {{ True
> }}
>
> where "world \sigma" is "World satisfaction", which says that all the
> invariants
> that have been allocated so far hold (new invariants can be allocated any
> time).
>
It seems like these "True"s also be "False"s if the semantic removed
threads after they terminate.

>  "Hold" here really means "we own the resources to justify them", and they
> are
> of course starred together.  There's also a "state interpretation"
> predicate
> supplied by whoever instantiate the language with Iris, which translate the
> shared state \sigma into an iris assertion (usually about owning some ghost
> state that is hence kept in sync with the physical state).  It's like
> another
> invariant, that connects the physical state to everything else.
>   Notably, Iris assertions are *not* predicates over the physical state of
> the
> machine, as is usually the case in separation logic.  They are predicates
> over
> the ghost state; the physical state comes in later and we use Iris'
> flexible
> ghost state to obtain the usual \mapsto predicate.  Thinking in terms of
> "fiction of separation", in Iris even the separation provided by \mapsto is
> fictional.  It is no more or less "real" than providing a fiction of
> \mapsto-with-fractions on top of a basic \mapsto. The Iris base logic
> doesn't
> even have a notion of a program state, so this is really the only way we
> can set
> these things up.
>
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).

>
> All of that said, this setup puts enough layers of abstraction between what
> users work with (Iris invariants) and the WP induction hypothesis that I
> have a
> hard time translating statements referring to the PC back into the Iris
> world --
> at least thinking in terms of a language like heap_lang, where the "PC"
> really
> is just a lambda term that still needs to be reduced.

This is understandable, there are a lot of moving pieces inside of Iris. I
think what you said is right though, a PC is just a lambda term.

>
> Kind regards,
> Ralf
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.mpi-sws.org/pipermail/iris-club/attachments/20181018/2d0e8293/attachment.html>