MIL

Architecture

MIL (Multithreaded Intermediate Language) is an assembly language targeted at an abstract multi-processor equipped with a shared main memory. Each processor consists of a series of registers and of a local memory for instructions and for local data. The main memory is divided into a heap and a run pool. The heap stores data and code blocks. Data blocks are represented by tuples and may be local to the processor for its exclusive use, or stored in the heap and shared amongst processors. A code block declares the registers it expects (including the type for each register), the required locks, and an instruction set. The run pool contains suspended threads waiting for a free processor.


Lock Discipline

We provide two distinct access privileges to shared tuples: read-only and read-write, the latter mediated by locks. A get and set lock instruction is used to obtain a lock, thus allowing a thread to enter a critical region. Threads read and write from the shared heap via conventional load and store instructions. The policy for the usage of locks (enforced by the type system) is depicted in the following figure, where λ denotes a lock singleton type and Λ the set of locks held by the thread (the thread's permission). Specifically, the lock discipline enforces that:

  • (i) before lock creation, λ is not a known lock;
  • (ii) before test and set lock, the thread does not hold the lock;
  • (iii) before accessing the heap, the thread holds the lock;
  • (iv) unlocking only in possession of the lock;
  • (v) thread termination only without held locks.

  • Type System

    The type system guarantees that well-typed programs are free from race conditions and deadlock states. The first property is achieved by imposing a discipline on the use of locks (through singleton types); the second property is achieved through polymorphic annotations dictating the order by which locks are closed. The type system refuses programs whose threads depend on each other, while acquiring locks cyclically.

    Since locks order annotation can cause unnecessary complexity in the process of code generation we have made these optional in MIL. The MIL interpreter infers, at loading time, polymorphic lock-order annotations. The inference collects local restrictions that are passed to an SMT solver that ascertains its consistency.


    Team

  • Vasco Vasconcelos (FCUL)
  • Francisco Martins (FCUL)
  • Tiago Cogumbreiro (PhD, Fcul)
  • Roberto Silva (MsC, Fcul)