@conference {14688,
	title = {Dynamically checking ownership policies in concurrent c/c++ programs},
	booktitle = {Proceedings of the 37th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages},
	series = {POPL {\textquoteright}10},
	year = {2010},
	month = {2010///},
	pages = {457 - 470},
	publisher = {ACM},
	organization = {ACM},
	address = {New York, NY, USA},
	abstract = {Concurrent programming errors arise when threads share data incorrectly. Programmers often avoid these errors by using synchronization to enforce a simple ownership policy: data is either owned exclusively  by a thread that can read or write the data, or it is read owned  by a set of threads that can read but not write the data. Unfortunately, incorrect synchronization often fails to enforce these policies and memory errors in languages like C and C++ can violate these policies even when synchronization is correct. In this paper, we present a dynamic analysis for checking ownership policies in concurrent C and C++ programs despite memory errors. The analysis can be used to find errors in commodity multi-threaded programs and to prevent attacks that exploit these errors. We require programmers to write ownership assertions that describe the sharing policies used by different parts of the program. These policies may change over time, as may the policies{\textquoteright} means of enforcement, whether it be locks, barriers, thread joins, etc. Our compiler inserts checks in the program that signal an error if these policies are violated at runtime. We evaluated our tool on several benchmark programs. The run-time overhead was reasonable: between 0 and 49\% with an average of 26\%. We also found the tool easy to use: the total number of ownership assertions is small, and the asserted specification and implementation can be debugged together by running the instrumented program and addressing the errors that arise. Our approach enjoys a pleasing modular soundness property: if a thread executes a sequence of statements on variables it owns, the statements are serializable within a valid execution, and thus their effects can be reasoned about in isolation from other threads in the program.},
	keywords = {concurrency, Debugging, Dynamic analysis, Security, Testing, tools},
	isbn = {978-1-60558-479-9},
	doi = {10.1145/1706299.1706351},
	url = {http://doi.acm.org/10.1145/1706299.1706351},
	author = {Martin,Jean-Phillipe and Hicks, Michael W. and Costa,Manuel and Akritidis,Periklis and Castro,Miguel}
}
@conference {16384,
	title = {The Java memory model},
	booktitle = {Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages},
	series = {POPL {\textquoteright}05},
	year = {2005},
	month = {2005///},
	pages = {378 - 391},
	publisher = {ACM},
	organization = {ACM},
	address = {New York, NY, USA},
	abstract = {This paper describes the new Java memory model, which has been revised as part of Java 5.0. The model specifies the legal behaviors for a multithreaded program; it defines the semantics of multithreaded Java programs and partially determines legal implementations of Java virtual machines and compilers.The new Java model provides a simple interface for correctly synchronized programs -- it guarantees sequential consistency to data-race-free programs. Its novel contribution is requiring that the behavior of incorrectly synchronized programs be bounded by a well defined notion of causality. The causality requirement is strong enough to respect the safety and security properties of Java and weak enough to allow standard compiler and hardware optimizations. To our knowledge, other models are either too weak because they do not provide for sufficient safety/security, or are too strong because they rely on a strong notion of data and control dependences that precludes some standard compiler transformations.Although the majority of what is currently done in compilers is legal, the new model introduces significant differences, and clearly defines the boundaries of legal transformations. For example, the commonly accepted definition for control dependence is incorrect for Java, and transformations based on it may be invalid.In addition to providing the official memory model for Java, we believe the model described here could prove to be a useful basis for other programming languages that currently lack well-defined models, such as C++ and C$\#$.},
	keywords = {concurrency, java, memory model, Multithreading},
	isbn = {1-58113-830-X},
	doi = {10.1145/1040305.1040336},
	url = {http://doi.acm.org/10.1145/1040305.1040336},
	author = {Manson,Jeremy and Pugh, William and Adve,Sarita V.}
}
