Amphitéâtre MJK
6 May 2013 - 14h00
Towards efficient and secure shared memory applications (Phd Defense)
by Emmanuel Sifakis from Verimag/UJF
6 May 2013 - 14h00
Towards efficient and secure shared memory applications (Phd Defense)
by Emmanuel Sifakis from Verimag/UJF
Abstract: The invasion of multi-core and multi-processor platforms on all aspects of
computing makes shared memory parallel programming mainstream.
Yet, the fundamental problems of exploiting parallelism efficiently and correctly
have not been fully addressed.
Moreover, the execution model of these platforms (notably the relaxed memory models
they implement) introduces new challenges to static and dynamic program analysis.
In this work we address 1) the optimization of pessimistic implementations of
critical sections and 2) the dynamic information flow analysis for parallel
executions of multi-threaded programs.
Critical sections are excerpts of code that must appear as executed atomically.
Their pessimistic implementation reposes on synchronization mechanisms, such as
mutexes, and consists into obtaining and releasing them at the beginning and end
of the critical section respectively.
We present a general algorithm for the acquisition/release of synchronization mechanisms
and define on top of it several policies aiming to reduce contention by minimizing the
possession time of synchronization mechanisms.
We demonstrate the correctness of these policies (i.e., they preserve atomicity
and guarantee deadlock freedom) and evaluate them experimentally.
The second issue tackled is dynamic information flow analysis of parallel executions.
Precisely tracking information flow of a parallel execution is infeasible due to
non-deterministic accesses to shared memory.
Most existing solutions that address this problem enforce a serial execution of the
target application.
This allows to obtain an explicit serialization of memory accesses but incurs both
an execution-time overhead and eliminates the effects of relaxed memory models.
In contrast, the technique we propose allows to predict the plausible serializations
of a parallel execution with respect to the memory model.
We applied this approach in the context of taint analysis , a dynamic information
flow analysis widely used in vulnerability detection.
To improve precision of taint analysis we further take into account the semantics
of synchronization mechanisms such as mutexes, which restricts the predicted
serializations accordingly.
The solutions proposed have been implemented in proof of concept tools which allowed
their evaluation on some hand-crafted examples.
