Email Gateway (Aug 19 2022 at 17:24): Email Gateway (Aug 19 2022 at 17:24):From: scott constable <sdconsta@syr.edu>
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
Email Gateway (Aug 19 2022 at 17:28):From: Gerwin Klein <Gerwin.Klein@nicta.com.au>
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
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.
Email Gateway (Aug 22 2022 at 08:58):From: scott constable <sdconsta@syr.edu>
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
Email Gateway (Aug 22 2022 at 09:08):From: Thomas Sewell <thomas.sewell@nicta.com.au>
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.
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.
Last updated: Apr 25 2024 at 12:23 UTC