On Concurrency Idioms and Program Analysis
This research delves into the impact of concurrency idioms on program analysis, emphasizing scalability and choosing optimal modeling languages. It focuses on improving verification, repair, and synthesis through a design-centric approach. The study explores different computational models, concurrency idioms, and techniques for program repair using blocking methods.
Download Presentation
Please find below an Image/Link to download the presentation.
The content on the website is provided AS IS for your information and personal use only. It may not be sold, licensed, or shared on other websites without obtaining consent from the author.If you encounter any issues during the download, it is possible that the publisher has removed the file from their server.
You are allowed to download the files provided on this website for personal or commercial use, subject to the condition that they are used lawfully. All files are the property of their respective owners.
The content on the website is provided AS IS for your information and personal use only. It may not be sold, licensed, or shared on other websites without obtaining consent from the author.
E N D
Presentation Transcript
On Concurrency Idioms and their Effect on Program Analysis Guy Katz and David Harel Weizmann Institute of Science
Overview Program analysis: verification, repair, synthesis, etc Very desirable, but very difficult State explosion How can we make analysis more scalable? 2
Improving Scalability Traditional focus: more efficient algorithms Symbolic model checking Abstraction / refinement Compositional verification And many others Our focus: how to choose the modeling language in a way that improves scalability A design for analysis approach 3
Choosing a Computational Model Goal: tailor a model for the task at hand Example: which programming models facilitate verification? Intuitively: DFA easier to verify than ?++ But programmers prefer ?++ A tradeoff Can we quantify it? 4
Our Goal Focus on individual concurrency idioms Idioms define inter-thread communication Which idioms are amenable to analysis? When? Idiom A Idiom B Idiom C Idiom D Idiom E Easy to analyze Retain just enough concurrency: keep things simple! 5
Program Repair A bug is found in existing software. Now what? Manual repair is difficult Automation is much needed 7
Repair Using Blocking Blocking: threads prohibit actions by other threads Very useful in repair Safety bugs: something bad happens Use blocking to prevent erroneous runs Liveness bugs: good things may never happen Use blocking to steer the execution towards good states Patches are non-intrusive "Non-Intrusive Repair of Safety and Liveness Violations in Reactive Programs", TCCI, 2014 8
Simple Safety Repair Some states are marked bad ?1 ?2 ?2 ?3 ?4 ?4 ?5 ?5 ?6 Finally, add a thread ( patch ) that blocks these edges
Additional Topics Compositional verification In some cases, simple idioms facilitate assume/guarantee reasoning Can even allow for automation (see talk later today) Succinctness Simple idioms are enough to write small programs Just as strong as very liberal models Automatic optimization of the program Relax certain synchronization constraints, while maintaining the program s semantics 10
Thank You! 11
