[bitc-dev] bitc and call/cc
swaroop.sridhar at gmail.com
Wed Aug 10 23:57:08 EDT 2005
Should Bitc consider reifying continuations?
I know that a decision to not do so was taken late last year, but the
reason I am reopening this issue is that it may be helpful in the logic
language to write assembly-like code that is well typed.
For example, consider:
If we HAVE to write the following sequence in assembly for performance
mov $0, %ecx
f3: add %eax, %ebx
cmp %ebx, 0
This sequence has no privileged instructions, but uses ad hoc control
transfer. The original idea was to present the logic system with a stub,
or a high-level equivalent of such a sequence. However, if we use
call/cc, it might be possible to prove properties about code sequences
that "look" very much like the above assembly language sequence.
(call/cc (lambda m
(let f1:(cont ()) (mutable m) ;; **1
(call/cc (lambda k (begin (set! ecx 0) (set! f1 k))))
(set! ecx (+ ecx 1))
(call/cc (lambda f2
(begin ;; **2
(set! ebx (+ eax ebx))
(if (== ebx 0) (throw f1 ()) (throw f2 ())))
(set! ecx (- %ecx 1))
**1 The only reason to annotate f1 with its type is to ward off any
concerns about value restriction
**2 I am not capturing f3 for simplicity as it is never thrown.
The second code fragment achieves the same effect as the first, but is
fully typed (barring any errors I may have made), and we can have some
hope that the control flow can be tracked by the verification engine.
However, very soon, one will write:
(call/cc (lambda k (set! f1 k)))
And, I am not sure whether the proof system will reach a fix point
without itself looping for ever in this case.
More information about the bitc-dev