[Haifux] Fwd: M.Sc. Thesis Seminar by Michael Kuperstein

[Orna Agmon Ben-Yehuda]

Hello all,
During Eli Billauer's PCI talk we had a brief discussion regarding the
necessity of barriers and the approach of "placing a barrier everywhere".
Michael Kuperstein's work refers exactly to this
point: automatically finding where a barrier is really needed, thus saving
long discussions on one hand, and unnecessary inefficiency on the other. He
will present his thesis this Wednesday at 12:30.
Orna.


----- Forwarded message from Graduate Seminar Announcement
<gradweb at CS.TECHNION.AC.IL> -----
   Date: Sun, 22 May 2011 12:30:23 +0300
   From: Graduate Seminar Announcement <gradweb at CS.TECHNION.AC.IL>
Reply-To: Graduate Seminar Announcement <gradweb at CS.TECHNION.AC.IL>
 Subject: M.Sc. Thesis Seminar by Michael Kuperstein
     To: CS-GRAD-SEMINARS-L at LISTSERV.TECHNION.AC.IL

Time and Place: 25/05/2011 12:30 in Taub 601
Speaker: Michael Kuperstein
Title: Preserving Correctness Under Relaxed Memory Models
Supervisor: Dr. Martin Vechev and Dr. Eran Yahav
Abstract:
We present an approach for automatic verification of concurrent programs
running under relaxed memory models. Verification under relaxed memory
models
is a hard problem. Given a finite state program and a safety specification,
verifying that the program satisfies the specification under a sufficiently
relaxed memory model is undecidable. For somewhat stronger memory models,
the
problem is decidable but has non-primitive recursive complexity.
We use abstract interpretation to provide a verification procedure for
programs
running under relaxed memory models. Our main contributions are:

-- A family of partial-coherence abstractions, which partially preserve
information required for memory coherence and consistency, while allowing
effective verification.

-- A framework for automatic repair of programs. Given a program, a
specification and a description of the memory model, our framework computes
a
set of constraints that guarantee the correctness of the program under the
memory model. The framework then realizes those constraints syntactically as
"memory fences", hardware instructions that ensure the constraints are never
violated.

We implemented our approach in a tool called BLENDER and used it to infer
correct and efficient placements of memory fences for several nontrivial
algorithms, including practical concurrent data structures and mutual
exclusion primitives.



----
This email was automatically generated.
For the full list of seminars and colloquiums,
see the faculty web page http://www.cs.technion.ac.il/he/.
For regulations on how to announce Ph.D. and M.Sc. seminars,
see http://www.cs.technion.ac.il/he/graduate/faq/seminar/

----- End forwarded message -----





-- 
Orna Agmon Ben-Yehuda.
http://ladypine.org
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://haifux.org/pipermail/haifux/attachments/20110522/12188979/attachment.html