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?