Simplifying Concurrent Programming with Transactional Memories

Parosh Aziz Abdulla1, Mohamed Faouzi Atig1, Zeinab Ganjei2, Ahmed Rezine2and Yunyun Zhu1 1. Uppsala University, Sweden 2. Link ping University, Sweden FMCAD 2015 FMCAD 2015

Transactional memories Formal model Small model theorem Limit the analysis to a finite number of variables Verification algorithm for cache coherence Backward reachability analysis with monotonic abstraction Prototype Two cache protocols verified

To simplify concurrent programming Init: x = 0 void add() { atomic { int t = x; t = t + 5; x = t; void add() { atomic { int t = x; t = t + 10; x = t; } } } } Thread 1 Thread 2 transaction transaction

Thread1 int t t = Thread2 int t t = x = t read x: 0 0 read x: int t = = t + 5 t = x x t + 5 read x: 0 0 read x: int t = = t + 10 x = t t = x x t + 10 Conflict! Conflict! write write x: x: 10 10 x = t x = t write write x: x: 5 5 write write x: x: 5 5 commit commit commit commit abort abort Init: x = 0 Properties of TMs: void add() { atomic { int t = x; t = t + 5; x = t; x = t; void add() { atomic { int t = x; t = t + 10; x = t; x = t; int t = x; t = t + 5; int t = x; t = t + 10; Atomicity Isolation } } } } Thread 1 Thread 2

Thread1 int t t = Thread2 int t t = x = t read x: 0 0 read x: int t = = t + 5 t = x x t + 5 read x: read x: 0 0 int t = = t + 10 x = t t = x x t + 10 write x: write x: 10 10 x = t x = t write x: write x: 5 5 write x: write x: 5 5 commit commit commit commit abort abort Init: x = 0 void add() { atomic { int t = x; t = t + 5; x = t; void add() { atomic { int t = x; t = t + 10; x = t; } } Hardware Hardware TM TM } } Thread 1 Thread 2

Thread1 int t t = Thread2 int t = = t + 5 t = x x t + 5 int t t = int t = = t + 10 x = t t = x x t + 10 x = t x = t x = t Conflict manager Decide if an instruction can be executed commit commit commit commit abort abort instruction instruction response response Conflict manager Conflict manager Cache protocol Adapted with TM context data state line data state line Cache C2 2 Cache C1 1 Cache C Cache C x y z x y z I I I I I I 0 0 0 0 0 0 data state line Memory Memory x y z I I I 0 0 0

Thread1 Thread2 Thread1 w write x Thread2 rite x write x write x read x write x read x write x write x write x Trace not allowed! allowed Trace not allowed! allowed Trace Trace Write within a transaction Modified Modified commit commit commit commit commit commit commit commit abort abort Commit Commit Exclusive Exclusive Filter Filter instruction instruction response response Conflict manager Conflict manager Shared Shared data state line data state line Cache C2 2 Cache C1 1 Cache C Cache C x y z x y z I I I I I I 0 0 0 0 0 0 TMI M M I TMI M M M Abort Abort Invalid Invalid Incoherent states! Incoherent states! state line Read while another writes within a transaction data Memory Memory x y z I I I 0 0 0

Threadn Thread1 write x read y commit Thread2 Thread2 Thread2 Thread1 w write x read y commit write Thread1 write x write x read y commit rite x read y commit write y y write x write y read x write y read x read z write z read z write z write y ... write y ... write x r read x abort write x ead x abort commit write y y commit write abort abort write x abort abort write x Verification of coherence in presence of filters commit write y commit write y commit write z commit write z commit abort . . . . commit abort . . . . . . . . . . . . . . . . instruction response instruction response instruction instruction response response Conflict manager Filter Conflict manager Filter Challenges: Unbounded number of transactions Cache C1 1 line Cache C Cache C Cache C1 1 Cache C2 2 data 0 0 Cache C data 0 0 0 0 Cache Cn n data state I I Cache C data state TMI I I TMI state state I TMI I state line data line line line state data line x y Cache C1 1 Cache Cn n Cache C1 1 Cache C2 2 Cache C2 2 Cache C Cache C Cache C Cache C x y z x x y x x I I I I I I I 0 0 0 0 0 0 0 0 0 Cache C I I M Unbounded number of threads ... y z z ... y ... ... ... 0 0 0 ... ... y z z z TMI Unbounded number of variables data 0 0 0 state state I line x y y data state line data 0 line x Memory Memory Memory Memory Memory Memory x y z z z I I I I 0 0 0 0 0 Memory Memory ... I I I I

Formal model for protocols with filters Small model theorem Reduces the problem to finite number of variables Backward reachability analysis Prototype

Configuration Maps each cache line to a state Transitions: Concerns the same cache line of different threads required E, TI, I , forbidden TMI , broadcast{E S}S I All the remote cache lines of M transits to S All the remote cache lines of x in M transits to S None remote cache line of x is TMI None remote cache line of is TMI in At least one remote cache line of At least one remote cache line of x is E, TI or I is E, TI or I Cache C line Cache C1 1 Cache C line Cache C2 2 Cache C line Cache C3 3 state state state E S state I S state I x y z x y z I E I I x y z I I I TI TMI local local remote remote remote remote

Thread2 Thread1 w write x rite x write x write x Finite set of forbidden patterns write, commit commit Forbidden pattern Forbidden pattern commit commit write, x x, t , t1 1 write, x, t write, x, t2 2 commit, t1 1 commit, t commit, t commit, t2 2 response response instruction instruction Filter Filter write, Trace not allowed! write, x x, t Trace not allowed! write, x x, t write, , t2 2 write, write, x x, t , t1 1 write, write, y y, t , t2 2 , t2 2 read, z z, t read, , t1 1 commit, commit, t t2 2 commit, commit, t t2 2 write, write, x x, t , t1 1 commit, t t2 2 commit, commit, t t2 2 commit, trace trace Cache C Cache C1 1 Cache C2 2 line Cache C Cache C3 3 line Cache C state line state state x y z x y z I I I x y z I I I I I I

Thread2 Thread1 w write x Thread2 Thread1 w write x rite x rite x r read y write x commit ead y write x commit Reduces the analysis to a finite number of variables w write z rite z write x write x commit commit commit commit commit commit write, x x, t write, , t2 2 commit, t t2 2 commit, commit, commit, t t1 1 write, write, x x, t , t1 1 read, read, y y, t , t2 2 write, z z, t write, , t1 1 write, x x, t write, , t2 2 commit, t t2 2 commit, response commit, t t1 1 response commit, write, x x, t write, , t1 1 instruction instruction Incorrect commit, commit, t t2 2 commit, t commit write, x x, t write, , t2 2 write, x x, t write, , t1 1 , t1 1 Filter Filter Reaches incoherent state, and passes the filter Cache C Cache C1 1 Cache C Cache C2 2 line state M M line state M M x y z x y z I I I I I I Only x involved Only x involved E M

Define a well well- -quasi quasi- -order order on configurations Prove transition relation is monotonic monotonic Provide an algorithm to compute the set of predecessors predecessors of an upward closed set Achievable with techniques Achievable with techniques

Define a well well- -quasi quasi- -order order on configurations Conf1 Conf2 Cache C line Cache C1 1 Cache C line Cache C2 2 Cache C line Cache C3 3 Cache C line Cache C1 1 Cache C line Cache C2 2 state state state state state x y z x y z S E S I I x y z S I I x z x z S E S I TMI

Prove transition relation is monotonic monotonic C C2 2 Conf2 Conf4 C C1 1 C C3 3 x x x S S I I Due to forbidden sets in transitions Conf1 Conf3 C C1 1 C C2 2 C C2 2 C C1 1 forbidden {S, E}E I x x x x I E I I

Define a well well- -quasi quasi- -order order on configurations Monotonic abstraction needed Monotonic abstraction needed Prove transition relation is monotonic monotonic

Incoherent states representable by finite caches M M I I S M M I M M With more caches still incoherent Minimal element Minimal element Upward closed sets: symbolic representations for incoherent states

Monotonic abstraction Monotonic abstraction Start from bad set t t1 1 t t2 2 Compute the set of predecessors, and make it upward-closed if needed t t2 2 t t3 3 Init = ? Init = ? Stop if no more new configuration discovered. t t1 1 A searching branch closed if The minimal element is subsumed By an older minimal element t t3 3 Trace (t fails the filter Trace (t3 3, t fails the filter , t2 2) ) The trace fails the filter

Extension of Zaama, which implements constrained monotonic abstraction Applied to Two cache protocols With six filters Results obtained a 2.9 Ghz Intel Core i7 with 8GB of RAM

Cache protocol (filter) #rules #bad states Reachable(Y/N) Execution time UTCP (serial. filter) 70 47 Yes, bad state (M, M) 117.3s TMESI (serial. filter) 42 38 Yes, bad state (M, M) 35.8s

Formal model for protocols with filters Small model theorem Reduces the problem to finite number of variables Backward reachability analysis Prototype