[Iris-Club] Using Iris

[Gregory Malecha]

Hi, Ralf --

This is an interesting conversation, I'm learning a lot, so thanks.

On Fri, Oct 12, 2018 at 6:57 AM Ralf Jung <jung at mpi-sws.org> wrote:

> Hi,
>
> >     Yes, if we have a triple for the continuation, we can just use that
> same
> >     postcondition.  We could likely have done the same thing in
> lambdaRust, but that
> >     would be one more parameter to carry around.  I think that would
> amount to
> >     making `cont_postcondition` a parameter here [1] and here [2].
> >
> > This makes sense, simplicity is a fine motivation for using True. I
> would be
> > willing to bet that if you globally replaced True with False, everything
> would
> > still work out (parametricity by sed!).
>
> I know for a fact that this is true because we started with `False`.
> Well, true with one exception: The final soundness proof that "closes" the
> type
> system uses `\ x. ()` as the final continuation, and has to prove it
> satisfies a
> triple with the `cont_postcondition`.  That's the one place where we need
> `True`.
>
This makes sense, you definitely need something *outside the system to
supply the final continuation*. In a normal C language, that continuation
is written in assembly and probably not expressible in Rust (it involves an
OS syscall), it is what tears down the runtime system. The great thing
about Iris and RustBelt is that since WP is not tied to the language, then
you could actually use Iris to prove that C code correct (with an
appropriate assumption on the syscalls provided by the operating system).

>
> >     On our case, that is exactly the problem. If halt halts the machine,
> it cannot
> >     have post-condition false. I guess we could define the operational
> semantics of
> >     halt to be "infinite loop", and then indeed postcondition false
> would work, but
> >     that didn't seem like a nice choice to us. So instead "halt" is just
> "()" [3] --
> >     unit, a term that is immediately done computing, and we use
> postcondition true.
> >
> > I think this is because usually "the machine is off" is not a state of
> the
> > system. If you wanted to add a true "off" state to the system, then (I
> think)
> > things would work out pretty easily. Simply interpret your predicates as
> "state
> > = on -> P". Since "state = off" has no transitions (or the identity
> transition,
> > however is more convenient to define it) the invariant is trivially
> preserved by
> > its steps.
>
> 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 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.

> 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.

>
> > There are three reasons that I like False, though they are matters of
> taste:
> >
> > 1. The reason that False makes sense to me is that callers of a function
> with a
> > False post-condition do not need to specify what happens after the
> function
> > returns, because they know that False it provable if the function
> returns so
> > they can simply eliminate that proof. Consider `WP (if (x == 0) {
> halt(); } else
> > { return 0; }) { \ ret => ret = 0 }`. This program will never fail to
> execute,
> > so one could argue that the weakest pre-condition should be True, but if
> halt
> > has post-condition True, then the weakest precondition is actually `x <>
> 0`.
>
> That still looks like a somewhat different setup than ours -- the
> postcondition
> is *always* `True` for us, and `return` would actually be a continuation (a
> lambda term, because we are just encoding this in lambda calculus) that
> you call
> and that has *precondition* "input is 0".  So if you translate your
> example to
> our setting, you do get the uniformity you are looking for.
>
> > 2. Another argument for this could be that the globalized program
> invariant
> > implies some safety condition trivially. Suppose, for example, I have a
> program
> > such as: { x <> 0 } diverge(); { True }
> > If I expand this out into a "whole system" invariant, I would get
> something like
> > "(pc = 0 -> x <> 0) /\ (pc = 1 -> True)" (assuming appropriate pc
> variables).
> > Simply looking at this assertion, I don't know that `x <> 0`. In order
> to prove
> > that `x <> 0` is an invariant of my system, then I need to know that `pc
> = 1 ->
> > False` which I haven't proven.
>
> Hm, I have a hard time translating this to Iris where we usually handle
> invariants differently.
>
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.


>
> > 3. `forall x, WP x False |-- WP x True` but not vice versa. If both are
> > provable, then why not prove something stronger? :-)
>
> I got nothing to add to that. ;)
>
> >     I agree that makes a lot of sense. I am just wondering, how do you
> model this
> >     "halt" instruction in your operational semantics?
> >
> > See above. If you wanted to do this at the OS level, then your False
> would be
> > scoped over the program's memory and things would work similarly. If this
> > program is running, then the invariant holds, if the program is not
> running, you
> > can't start running it (without re-initializing it).
>
> I am slightly puzzled by your use of the term "invariant" here (and in some
> places above).  We were talking about "halt" and postconditions, not about
> anything I would call "invariant", so I suspect our terminology is not
> entirely
> aligned.  We have a specific mechanism in Iris for sharing ownership across
> threads, by establishing an invariant on a piece of state and then sharing
> knowledge of that invariant with anyone else.  That's not what you refer
> to, I

think, but then I don't know which is "the invariant" that holds.
>
See above.

>
> 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/20181012/977a926f/attachment-0001.html>