Mil In Glua Techsessions '08

MIL

Multithreaded Intermediate Language Tiago Cogumbreiro [email protected] Joint work with Francisco Martins Vasco T. Vasconcelos Universidade de Lisboa

GLUA Tech Sessions ’08

MIL Motivation

Outline

1 Motivation 2 A Lock Discipline 3 Data Races 4 The Language 5 Examples

Singlecore

Multicore

MIL Motivation

Context

Fine-grained multithreading Thousand of threads

MIL Motivation

Goal

Concurrency primitives Shared memory Security properties: typed enforce a memory usage discipline

MIL Motivation

Our approach

Typed assembly language Support threads Flannagan’s and Abadi’s locking discipline

MIL Motivation

MIL’s Architecture

CPU core 1

CPU core N

registers

registers

local memory

local memory

run pool

heap

MIL A Lock Discipline

Outline

1 Motivation 2 A Lock Discipline 3 Data Races 4 The Language 5 Examples

MIL A Lock Discipline

/* * Lock surface. (Don’t forget to call Unlock) */ void nD3D9Surface::Lock(int &pitch, void** data)

The Nebula Device, a real-time 3D game/visualization engine.

MIL A Lock Discipline

What if someone forgets?

MIL A Lock Discipline

else if(wndPtr->irefCount < 0) { /* This else if is useful to monitor the WIN_ReleaseWndPtr function */ ERR("forgot a Lock on %p somewhere\n",wndPtr); } /* unlock all WND structures for thread safeness */ USER_Unlock(); WINE 20050211

MIL A Lock Discipline

/* This should never happen, otherwise someone forgot to get the HostEntry->lock! */ CODA_ASSERT(HostEntry->id == 0); CODA 5.3.20

MIL A Lock Discipline

Is that a solution?

MIL A Lock Discipline

Rules

Close known lock → acquires permission to unlock Obligated to unlock the lock or transfer that obligation

MIL Data Races

Outline

1 Motivation 2 A Lock Discipline 3 Data Races 4 The Language 5 Examples

What if I could change your poker’s hand?

MIL Data Races

Mutual Exclusion

One thread (or process) alone handles the resource.

MIL Data Races

Enforcing mutual exclusion

Core 1

Core 2

Core 3

MIL Data Races

No race conditions!

MIL The Language

Outline

1 Motivation 2 A Lock Discipline 3 Data Races 4 The Language 5 Examples

MIL The Language

Memory and control flow

Move r := v Alloc r := malloc [~τ ] Load r := v [n] Store r [n] := v Jump jump v Conditional Jump if r = v jump v No call stack.

MIL The Language

Security properties

Unset register are not read Loads and stores target tuples Stores of the expected type only Jump to code blocks only Arithmetic only with registers holding integers

MIL The Language

Threads

Create fork v Finish yield Cooperative threads

MIL The Language

Security properties

Zero closed locks in order to yield Forking code blocks only

MIL The Language

Test and set

Atomic operation: int testSet(int *ptr) { int v = *ptr; *ptr = 1; return v; }

MIL The Language

Implementing a lock with test and set

Case 1 → 1: was locked Case 0 → 1: was unlocked

MIL The Language

Locks

Create α, r := newLock Acquire r := testSetLock v Release unlock v Share share r guarded by α

MIL The Language

Security properties

Test and set lock open locks Unlock closed locks, with permission Target locks (type)

MIL Examples

Outline

1 Motivation 2 A Lock Discipline 3 Data Races 4 The Language 5 Examples

MIL Examples

Factorial fract (r1:int) { r2 := 1 if r1 = 0 jump fractFinish jump doFract } doFract (r1:int, r2:int) { if r1 = 1 jump fractFinish r2 := r2 * r1 r1 := r1 - 1 jump doFract } fractFinish (r2:int) { -- do some work }

MIL Examples

Creating a tuple

prepare () { r1 := malloc [int, int] r1[0] := 10 r1[1] := 20 share r1 guarded by l jump compute } compute (r1: ^l) { -- do some work }

MIL Examples

Spin-lock

spinLock (r1:^l, r2:^l) { r3 := testSetLock r1 if r3 = 0 jump criticalRegion jump spinLock } criticalRegion (r1: ^l, r2:^l) requires (l) { r1[0] := 10 unlock r1 yield }

MIL Examples

Sleep-lock sleepLock (r1:^l, r2:^l) { r3 := testSetLock r1 if r3 = 0 jump criticalRegion fork sleepLock yield } criticalRegion (r1: ^l, r2:^l) requires (l) { r1[0] := 10 unlock r1 yield }

MIL Examples

Omitted features

Universal quantifier Existential quantifier Recursive type Read-only tuples

MIL Examples

Further work

Compare and swap for lock-free data structures Dead-lock freedom

MIL Examples

For publications and implementation, please refer to http://gloss.di.fc.ul.pt/mil Thank you. Any questions?