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 <grad...@cs.technion.ac.il> ----- Date: Sun, 22 May 2011 12:30:23 +0300 From: Graduate Seminar Announcement <grad...@cs.technion.ac.il> Reply-To: Graduate Seminar Announcement <grad...@cs.technion.ac.il> Subject: M.Sc. Thesis Seminar by Michael Kuperstein To: cs-grad-seminar...@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
_______________________________________________ Haifux mailing list Haifux@haifux.org http://hamakor.org.il/cgi-bin/mailman/listinfo/haifux