Tata Institute of Fundamental Research
Fence Synthesis Using Happens-before Formulas
Seminar
Speaker:
Shikhar Pandya (Visiting Student
School of Technology and Computer Science
Tata Institute of Fundamental Research
Homi Bhabha Road
Navy Nagar
Mumbai 400005)
Organiser:
Ashutosh Gupta
Date:
Wednesday, 27 Apr 2016, 16:00 to 17:00
Venue:
A-201 (STCS Seminar Room)
(Scan to add to calendar)
Abstract:
Abstract: Weak memory adds many behaviors in a concurrent program that are unexpected by the most programmers. The weak memory behaviors can be removed by placing memory fences in the programs. For performance, one should only add minimal number of fences such that there are no unwanted behaviors. In this paper, we present a novel method for synthesizing fences that disallow behaviors that are due to week memory and violate a safety property of a straight line concurrent program. Our method constructs a formula that encodes all violating executions of the program under weak memory and iteratively constructs a happens-before formula over memory events that represents memory event orderings that leads to error for some inputs. Afterwards, our method searches for event cycles encoded in the formula and optimally introduces fences such that the cycles are removed from the program behavior. We have implemented the above method in Tara. Our tool supports TSO, PSO, and RMO memory models. We applied Tara on benchmarks, and compared the performance with fence synthesis tools Glue and Memorax.
| Speaker: | Shikhar Pandya (Visiting Student School of Technology and Computer Science Tata Institute of Fundamental Research Homi Bhabha Road Navy Nagar Mumbai 400005) |
| Organiser: | Ashutosh Gupta |
| Date: | Wednesday, 27 Apr 2016, 16:00 to 17:00 |
| Venue: | A-201 (STCS Seminar Room) |
(Scan to add to calendar)
Abstract:
Abstract: Weak memory adds many behaviors in a concurrent program that are unexpected by the most programmers. The weak memory behaviors can be removed by placing memory fences in the programs. For performance, one should only add minimal number of fences such that there are no unwanted behaviors. In this paper, we present a novel method for synthesizing fences that disallow behaviors that are due to week memory and violate a safety property of a straight line concurrent program. Our method constructs a formula that encodes all violating executions of the program under weak memory and iteratively constructs a happens-before formula over memory events that represents memory event orderings that leads to error for some inputs. Afterwards, our method searches for event cycles encoded in the formula and optimally introduces fences such that the cycles are removed from the program behavior. We have implemented the above method in Tara. Our tool supports TSO, PSO, and RMO memory models. We applied Tara on benchmarks, and compared the performance with fence synthesis tools Glue and Memorax.