Compiling The π-calculus Into A Multithreaded Typed Assembly Language (presentation)

Compiling the π-calculus into a Multithreaded Typed Assembly Language Tiago Cogumbreiro [email protected] Joint work with Francisco Martins Vasco T. Vasconcelos Universidade de Lisboa

Workshop on Places ’08

Goal Compilation from the π-calculus into a multithreaded typed assembly language (MIL) Result Type-preserving translation

Source language: typed π-Calculus

P ::=

Processes

0

nil

xhv i

output

x(y ).P

input

P |Q

parallel

! x(y ).P

replicated input

(ν x : (T ))P restriction

v ::=

Values . . . 0 . . . integer

x T ::= int (T )

name Types integer type channel type

Target language: MIL (architecture)

CPU core 1

CPU core N

registers

registers

instruction cache

instruction cache

run pool

heap

Target language: MIL (features)

Locks

Threads

Create α, r := newLock b Acquire r := testSetLock v Release unlock v

I

Create fork v Finish yield

Type system enforces race-condition freedom

Translating processes and values

P

Environment fn(P) [[P]]

x

State Messages Processes

Translation of nil processes

[[0]]

yield

Translation of nil processes

[[0]]

yield

CPU core 1

CPU core 1

registers

registers

[[0]]

yield

Translation of output processes [[xhv i]]

jump send(x, v )

Translation of output processes [[xhv i]]

jump send(x, v ) Supporting Library enqueue;yield

no

o pr

es ss e c

send [[xhv i]]

[[P{v /y }]] reduce

Translation of parallel processes

[[P | Q]]

fork [[Q]]; jump [[P]]

Translation of parallel processes

[[P | Q]]

fork [[Q]]; jump [[P]]

CPU core 1

CPU core 1

registers

registers

[[P | Q]]

[[P]]

Thread pool

Thread pool [[Q]]

Translation of input processes [[x(y ).P]]

jump receive(x, P)

Translation of input processes [[x(y ).P]]

jump receive(x, P) Supporting Library enqueue;yield

s

ge

sa es

no

m

receive [[P{v /y }]]

[[x(y ).P]] reduce

Supporting library

I

Queue operations (creating, enqueueing, dequeueing)

I

Three public operations send, receive, and create channel

I

19 code blocks

I

34 type definitions

I

322 lines of MIL code

I

8 registers needed

I

Locks are abstracted from the translation function

Lock usage

I

Multiple readers on environments (no contention)

I

One lock per channel

Spin lock

s e n d [ a l p h a , t a u ] ( r 1 : tau , r 4 : ChannelType ( tau , a l p h a ) , r 5 : ˆ a l p h a ) { −− s p i n l o c k t o a c q u i r e t h e g l o b a l l o c k a l p h a r 2 := t s l S r 5 i f r2 = 0 −− a c q u i r e d t h e l o c k , unpack t h e c h a n n e l jump sendUnpack [ t a u ] [ a l p h a ] −− t r y a g a i n jump s e n d [ t a u ] [ a l p h a ] }

Trying to reduce

sendMessage [ alpha , tau ] ( r 1 : tau , r 2 : ChannelQueueType ( tau , a l p h a ) , r 3 : ˆ a l p h a ) r e q u i r e s ( alpha ; ; ) { −− g e t t h e s t a t e o f t h e c h a n n e l r 4 := C h a n n e l Q u e u e S t a t e ( r 2 ) i f r 4 = CHANNEL QUEUE WITH PROCS −− when t h e r e a r e , d e l i v e r t h e message : jump s e n d M e s s a g e R e d u c e [ t a u ] [ a l p h a ]

−− f l a g t h e c h a n n e l a s c o n t a i n i n g m e s s a g e s : C h a n n e l Q u e u e S t a t e ( r 2 ) := CHANNEL QUEUE WITH MSGS −− g e t t h e queue o f m e s s a g e s r 2 := ChannelQueueMsgs ( r 2 ) −− p u t t h e message ( r 1 ) i n t h e queue QueueAdd ( r2 , r1 , r4 , r1 , tau , a l p h a ) unlockE r3 yield }

Conclusions

I

Formalized translation in a multithreaded architecture

I

Type-preservation: If P is a well typed π-process, then [[P]] is a well typed MIL program

Future work

I

Simplifying the supporting library

I

Extend MIL (lock-free channels)

I

Correctness

I

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