ivory- Safe embedded C programming.

Copyright(c) 2014 Galois Inc.
Safe HaskellNone




This is an implementation of coroutines in Ivory. These coroutines:

  • may be suspended and resumed,
  • are parametrized over any memory-area type (Area),
  • cannot return values, but can receive values when they are resumed (though this is an incidental detail of the current implementation),
  • for now, can have only one instance executing at once, given a particular coroutine name and Ivory module.

Usage Notes

The coroutine itself is presented as a function which has one argument, yield. yield suspends the coroutine's execution at the point of usage.

coroutineRun (given an argument of false) then resumes the suspended coroutine at that point, passing in a value in the process.

Implementation Notes

This implementation handles a coroutine in the form of a single contiguous block of Ivory code. It turns this block into a single large C function, breaking it up into an initialization portion and a series of branches inside an infinite loop. Each branch represents a resume and suspend point within that block.

It was mentioned that yield suspends a coroutine for later resumption. The state of the computation to be resumed later - that is, its continuation - is stored in a C struct, not visible to the outer Ivory code, but denoted internally with a suffix of _continuation. This C struct contains a state variable and every local variable that is created.

At each yield, after collecting the current computation state into the continuation, the C function breaks out of its loop and returns.

The yield action is implemented as a sort of pseudo-function call which is given a purposely-invalid name (see yieldName). This Ivory call does not become an actual function call in generated code, but rather, the code is suspended right there. (See the extractLocals and addYield functions.)

The pseudo-function call returns a ConstRef to the coroutine's type. Of course, no actual function call exists, but the action itself still returns something - hence, Ivory code is able to refer to the return value of a yield. Dereferences to it via deref are turned to references to the continuation struct.

As this yield action is an Ivory effect, it can be passed at the Haskell level, but it cannot be passed as a C value. (If one could hypothetically run procPtr on it, then one could pass it around as a value, but any attempt to call it outside of the same coroutine would result in either an invalid function call, or a suspend & return of a different coroutine.)

data Coroutine a Source #

Concrete representation of a coroutine; use coroutine to produce one.




newtype CoroutineBody a Source #

The definition of a coroutine body, in the form of a function taking one argument: an Ivory effect that is the yield action which suspends the coroutine, and sets the point at which coroutineRun resumes it, passing a value.


CoroutineBody (forall s1 s2. (forall b. Ivory (Effects (Returns ()) b (Scope s2)) (Ref s1 a)) -> Ivory (ProcEffects s2 ()) ()) 

coroutine Source #


:: IvoryArea a 
=> String

Coroutine name (must be a valid C identifier)

-> CoroutineBody a

Coroutine definition

-> Coroutine a 

Smart constructor for a Coroutine