<div dir="ltr">Hello all,<div>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.<div>
Orna.<br><div class="gmail_quote"><br><br>
----- Forwarded message from Graduate Seminar Announcement<br>
<<a href="mailto:gradweb@CS.TECHNION.AC.IL">gradweb@CS.TECHNION.AC.IL</a>> -----<br>
Date: Sun, 22 May 2011 12:30:23 +0300<br>
From: Graduate Seminar Announcement <<a href="mailto:gradweb@CS.TECHNION.AC.IL">gradweb@CS.TECHNION.AC.IL</a>><br>
Reply-To: Graduate Seminar Announcement <<a href="mailto:gradweb@CS.TECHNION.AC.IL">gradweb@CS.TECHNION.AC.IL</a>><br>
Subject: M.Sc. Thesis Seminar by Michael Kuperstein<br>
To: <a href="mailto:CS-GRAD-SEMINARS-L@LISTSERV.TECHNION.AC.IL">CS-GRAD-SEMINARS-L@LISTSERV.TECHNION.AC.IL</a><br>
<br>
Time and Place: 25/05/2011 12:30 in Taub 601<br>
Speaker: Michael Kuperstein<br>
Title: Preserving Correctness Under Relaxed Memory Models<br>
Supervisor: Dr. Martin Vechev and Dr. Eran Yahav<br>
Abstract:<br>
We present an approach for automatic verification of concurrent programs<br>
running under relaxed memory models. Verification under relaxed memory models<br>
is a hard problem. Given a finite state program and a safety specification,<br>
verifying that the program satisfies the specification under a sufficiently<br>
relaxed memory model is undecidable. For somewhat stronger memory models, the<br>
problem is decidable but has non-primitive recursive complexity.<br>
We use abstract interpretation to provide a verification procedure for programs<br>
running under relaxed memory models. Our main contributions are:<br>
<br>
-- A family of partial-coherence abstractions, which partially preserve<br>
information required for memory coherence and consistency, while allowing<br>
effective verification.<br>
<br>
-- A framework for automatic repair of programs. Given a program, a<br>
specification and a description of the memory model, our framework computes a<br>
set of constraints that guarantee the correctness of the program under the<br>
memory model. The framework then realizes those constraints syntactically as<br>
"memory fences", hardware instructions that ensure the constraints are never<br>
violated.<br>
<br>
We implemented our approach in a tool called BLENDER and used it to infer<br>
correct and efficient placements of memory fences for several nontrivial<br>
algorithms, including practical concurrent data structures and mutual<br>
exclusion primitives.<br>
<br>
<br>
<br>
----<br>
This email was automatically generated.<br>
For the full list of seminars and colloquiums,<br>
see the faculty web page <a href="http://www.cs.technion.ac.il/he/" target="_blank">http://www.cs.technion.ac.il/he/</a>.<br>
For regulations on how to announce Ph.D. and M.Sc. seminars,<br>
see <a href="http://www.cs.technion.ac.il/he/graduate/faq/seminar/" target="_blank">http://www.cs.technion.ac.il/he/graduate/faq/seminar/</a><br>
<br>
----- End forwarded message -----<br>
<br>
<br>
</div><br><br clear="all"><br>-- <br>Orna Agmon Ben-Yehuda.<br><a href="http://ladypine.org">http://ladypine.org</a><br>
</div></div></div>