Concurrency model

Many concurrency models exist (actors with message passing, threads, coroutines, map-reduce, event systems, ...). We will try to find one which is as low-level as possible but still generic, as independent of a particular microprocessor architecture or operating system. In this way we hope to:

• express hight-performance algorithms
• define higher-level paradigms in a type-safe manner
• be as close as possible to the hardware to reduce hypothesis on unproven code.

Interaction with the hardware and OS

Coq is a purely functional language, so concurrency or imperative effects can only be encoded or axiomatized. We will use a kind of monadic system, in the spirit of Haskell, with defined operators to ensure consistency. These defined operators will then be compiled to an efficient and native implementation.

The hardware of a computer provides many facilities which are not captured by a λ-calculus based language, such as mutable data-structures, cheap exceptions, input-outputs, timers, threads, ... We chose to represent this set of features:

• global and shared mutable memory (with atomic reads and writes)
• outputs as non-blocking and always successful writes to an output channel
• inputs as interruptions

Exceptions or local states are not covered for now. We expect the user to explicitly encode them using option types or adding a local state as an explicit parameter to functions using it.

New (user or system) threads can be launched to handle each interruption, if the scheduler desires to, in order to improve performances. The programs should be written without any hypothesis about the scheduler. There is no explicit operator to start a new thread and improve performances of parallel algorithms. This may be added later.

With this model, interactions with the hardware and the OS are always non-blocking. An alternative approach could be based on:

• global and shared mutable memory (with atomic reads and writes)
• explicit threads
• blocking system calls

This corresponds more to standard APIs such as the Unix API and should be easier to use.

But we prefer the non-blocking model since it is more low-level. In assembly this would correspond to:

• DMA (Direct Memory Access)
• x86 OUT instruction
• interruptions