Re: [isabelle] Abruptly Terminating a State Monad



I guess the short summary here is that there won't be a quick fix. The
type of the state monad has to change.

Some kind of exception/state monad combination will be an appropriate
type for your function. So reboot() will be able to abort all subsequent
actions (exception monad) but keep the current state (state monad).

The problem is that AutoCorres won't produce such a monad, and the
bigger problem is that the C-parser won't assign appropriate semantics.
We've had this discussion at NICTA before - there was a fast abort
mechanism that would be useful in seL4 - but the problem is that
anything like this isn't really C. The only C approximation is
setjmp/longjmp which is horrible and isn't going to be supported.

In short, we don't really know what to do about this. It's clear there's
a lot of C code out there with nonreturning functions, so maybe we
should think about how to support it at the C semantics level. Having
AutoCorres deal with this by returning a more general monad type won't
be too difficult. But I think this is low priority for NICTA at the moment.

Cheers,
    Thomas.

P.S. The reason we had this discussion at NICTA before is to do with
seL4's design. It uses a syscall stack model, where every OS entry lives
on a newly created stack. This makes a convenient operation possible (if
written in assembly): a function which discards the running stack
entirely and either reenters the OS with new toplevel arguments or
returns to user level. I guess it's a lot like a reboot, only it happens
to be really fast. Supporting this would allow us to shrink the kernel
code a lot - there's lots of caller/callee pairs where the caller has to
check for failure, and where the callee could instead call the failure
handling mechanism then abort everything.



it would be convenient in OS's such as seL4 to implement the action that
aborts everything in the current system call stack, and either re-enters
the kernel or returns to user mode. A bit like rebooting, I suppose,
although much faster. The SIMPL semantics that the C semantics builds on
has an exception mechanism that would work for this purpose, but the
problem is that it isn't really C.



On 31/03/15 09:16, scott constable wrote:
Thanks Gerwin,

We've been toying with your ideas and a few others over the past week, and
have observed that both techniques you've described (MAGIC and making
reboot() "unreachable") amount to the same thing: stating preconditions
which ensure that reboot() is never called. While this helps us to reason
about program behavior when reboot() is called, it also prevents us from
reasoning about program behavior when reboot() is called. For example, we
could prove something like the following:

{ P s }
entire_program
{ True }!

where P is the conjunction of all the assumptions which need to hold in
order for entire_program to terminate properly (i.e. not call reboot()).

This, I believe, is essentially stating that "if P s holds, then
entire_program() terminates properly." But what we are more interested in
is proving the statement "entire_program will terminate properly *only if *P
s holds."

~Scott

On Fri, Mar 20, 2015 at 9:51 PM, Gerwin Klein <Gerwin.Klein at nicta.com.au>
wrote:

Hi Scott,

youâre right that this will not be properly representable in the monadic
framework AutoCorres uses, because that wants termination for everything.

Itâs conceivable that you might be able get away with manually defining
(axiomatising) reboot as MAGIC, i.e. the function that returns the empty
set and does not fail. Should be equivalent to a C-level specification that
claims the function terminates with post condition False.

Youâll need to think about what that really means, though, and if that
agrees with what you want to prove. I havenât thought too much about this,
might be that this is a more general way to deal with non-termination, or
it might break down at some point.

Depending on if it would be Ok to propagate âconditionâ up through your
preconditions, you could also model âreboot()â as âunreachableâ, i.e. a
function with precondition False, which will require you to prove that it
is never called. (This is what we use for âhalt()â, since we never want
that to happen.)

Cheers,
Gerwin

On 19 Mar 2015, at 3:37 am, scott constable <sdconsta at syr.edu> wrote:

Hi All,

I'm currently trying to reason in AutoCorres about a bit of code which
may
abruptly terminate. What I'm trying to prove is something like this:

{| <\lambda> s. True |}
interesting_function() {
    global_flag = 0;
    if (condition)
        reboot();
    else
        global_flag = 1;
    return;
}
{| <\lambda> s _. global_flag = 1 |}

Clearly, interesting_function() will only return with global_flag set to
1,
but I'm not sure how a state monadic framework could possibly model the
reboot() call. After interesting_function() returns, another function,
say
interesting_function2() will be called with global_flag=1 as a
precondition.

At a high level, I'm trying to prove reachability. That is,
interesting_function2() is reachable only if condition=false in
interesting_function1(). So it's also possible that I'm using entirely
the
wrong approach here.

Thanks in advance for any feedback.

~Scott Constable

________________________________

The information in this e-mail may be confidential and subject to legal
professional privilege and/or copyright. National ICT Australia Limited
accepts no liability for any damage caused by this email or its attachments.



________________________________

The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.