CakeML / cakeml

CakeML: A Verified Implementation of ML
https://cakeml.org
Other
946 stars 83 forks source link

Keyboard interrupts / asynchronous FFI events #783

Open sorear opened 4 years ago

sorear commented 4 years ago

A REPL is more useful if you can abort things that are taking too long.

This is immediate if you have threads (you can model an interrupted thread as never running again); conversely it might be as difficult as threads, since if you want to allow compiler transformations that reorder writes to heap objects (including various forms of dead store elimination and most advanced loop optimizations) the semantics need to include a memory model describing what could be visible out of order.

If this is thread-complete it's likely not worthy of further discussion but leaving this here in case anyone has clever ideas.

sorear commented 4 years ago

Idea from last night: add a FFI which snapshots the heap+stack+saved registers and restore them in a signal handler. Doubling the memory use isn't ideal but the semantics are very clear.