Performance-aware Synthesis for Concurrency

Speaker: Arjun Radhakrishna , IST Austria

Date: Tuesday, February 11, 2014

Time: 2:30 PM to 3:30 PM Note: all times are in the Eastern Time Zone

Refreshments: 2:15 AM

Public: Yes

Location: 32-G449

Event Type:

Room Description:

Host:

Contact: Armando Solar-Lezama, asolar@csail.mit.edu

Relevant URL:

Speaker URL: None

Speaker Photo:
None

Reminders to: seminars@csail.mit.edu, pl@lists.csail.mit.edu

Reminder Subject: TALK: Performance-aware Synthesis for Concurrency

Partial-program synthesis is a technique that allows programmer to
specify only part of the program imperatively and the rest of the
requirements declaratively. In the domain of concurrency, the input
usually consists of a non-deterministic partial program where the
programmer omits synchronization constructs. The synthesizer fills in
the appropriate synchronization to keep the program correct. However, a
major hurdle to adoption of these techniques is the performance of the
synthesized program. In this talk, I will present two different
approaches we have explored for making synthesis for concurrent programs
performance aware.

First, I will present an algorithmic method for the quantitative,
performance-aware synthesis. In addition to the partial-program, the
input consists of a non-deterministic partial program and of a
parametric performance model. The performance model, specified as a
weighted automaton, can capture system architectures by assigning
different costs to actions such as locking, context switching, and
memory and cache accesses. The quantitative synthesis problem is to
automatically resolve the non-determinism of the partial program so that
both correctness is guaranteed and performance is optimal. For
worst-case (average-case) performance, we show that the problem can be
reduced to 2-player graph games (with probabilistic transitions) with
quantitative objectives.

Second, I will present an alternative approach which tries to avoid
expensive synchronization constructs such as locks and atomic sections.
The synthesis procedure explores a variety of (sequential)
semantics-preserving program transformations for fixing concurrency
bugs. Classically, only one such transformation has been considered,
namely, the insertion of locks. Based on common manual bug-fixing
techniques used by Linux device-driver developers, we explore
additional, more efficient transformations, such as the reordering of
independent instructions. We evaluated our techniques on several
simplified examples of real concurrency bugs that occurred in Linux
device drivers.

Research Areas:

Impact Areas:

See other events that are part of the PL/SE Seminar Series 2013/2014.

Created by Armando Solar-Lezama Email at Monday, February 10, 2014 at 1:49 PM.