In this dissertation, I present a set of novel constraint-based thread-modular abstract-interpretation techniques for static analysis of concurrent programs. Specifically, I integrate a lightweight constraint solver into a thread-modular abstract interpreter to reason about inter-thread interference more accurately. Then, I show how to extend the new analyzer from programs running on sequentially consistent memory to programs running on weak memory. Finally, I show how to perform incremental abstract interpretation, with and without the previously mentioned constraint solver, by analyzing only regions of the program impacted by a program modification. I also demonstrate, through experiments, that these new constraint-based static analyzers are significantly more accurate than prior abstract interpretation-based static analyzers, with lower runtime overhead, and that the incremental technique can drastically reduce runtime overhead in the presence of small program modifications. / Ph. D.
| Identifer | oai:union.ndltd.org:VTETD/oai:vtechworks.lib.vt.edu:10919/84399 |
| Date | 25 July 2018 |
| Creators | Kusano, Markus Jan Urban |
| Contributors | Electrical and Computer Engineering, Wang, Chao, Hsiao, Michael S., Zeng, Haibo, Lee, Dongyoon, Schaumont, Patrick R. |
| Publisher | Virginia Tech |
| Source Sets | Virginia Tech Theses and Dissertation |
| Detected Language | English |
| Type | Dissertation |
| Format | ETD, application/pdf |
| Rights | In Copyright, http://rightsstatements.org/vocab/InC/1.0/ |
Page generated in 0.0023 seconds