Type-based race detection for Java

By Cormac Flanagan, Stephen N. Freund. ACM-SIGPLAN Symposium on Programming Language Design and Implementation, 2000

433 citations recorded by the source corpus.

Subfields: Artificial Intelligence, Hardware and Architecture, Information Systems

View Paper: https://www.semanticscholar.org/paper/6a1ae100d7447ab82a58cb8457540eb83cd808a6

How researchers see this paper

The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.

In Artificial Intelligence

In Hardware and Architecture

In Information Systems

Citations in the corpus

RELAY: static race detection on millions of lines of code (2007, background): “Early work includes the development of type systems that encode a static lockset ana lysis [9, 10].”
The Java memory model (2005, background): “An alternative is to to design a language that is completely free from data races [Reynolds 1978; Bacon et al. 2000; Flanagan and Freund 2000].”
Atomizer: a dynamic atomicity checker for multithreaded programs (2004, background): “This lockbased synchronization discipline is supported by a variety of type systems [21] [20] [19] [22] [8] [7] [28] and other static [49] [23] [10] [13] and dynamic [47] [11] [51] [42] [45] analyses.”
Using model checking to find serious file system errors (2004, background): “There has been much recent work on bug .nding, including both better type systems [DeLine and F¨ ahndrich 2001; Foster et al. 2002; Flanagan and Freund 2000] and static analysis tools [Das et al. 2002; Ball and Rajamani 2001; Coverity http://coverity.com; Bush et al. 2000; Engler et al. 2000;…”
KISS: keep it simple and sequential (2004, methodology): “The Race Condition Checker (RccJava) [16, 17] uses a type system to catch race conditions in Java programs.”
RacerX: effective, static detection of race conditions and deadlocks (2003, methodology): “[15] C. Flanagan and S. N. Freund.”
Enforcing high-level protocols in low-level software (2001, background): “propose a type system for Java to statically detect data races [6].”
Object race detection (2001, methodology): “It has been initially proposed and used by [6, 9] and was the foundation for several implementations of on-the- y [9, 26] as well as static race checkers [30, 8, 11].”
Formalising Java's Data Race Free Guarantee (2007, background): “The data race freedom can be established inside the program logics themselves, or using dedicated type systems [22, 23].”
EXE: automatically generating inputs of death (2006, background): “…static input generation Therehasbeenmuch recent work onstaticbug .nding,includingbettertype systems[DeLine andF¨ ahndrich 2001; Foster et al. 2002; Flanagan and Freund2000], static analysistools[Foster et al.2002;Ball andRajamani2001; Coverity;Das etal.2002;Flanagan et al.2002;Bush et…”
Ownership, encapsulation and the disjointness of type and effect (2002, background): “Boypati, Lee and Rinard’s work extends prior systems such as Guava [5], which also has a notion of thread ownership, and Flanagan and Freund’s [29] which parameterises classes by locks [29].”
Polyglot: An Extensible Compiler Framework for Java (2003, background): “A language might be extended to support annotations necessary for static verification of program correctness [24], more powerful static checking of program invariants [8, 12, 11], or heuristic methods [9].”
A system and language for building system-specific, static analyses (2002, methodology): “One of the most rigorous measurements of this overhead comes from Flanagan and Freund who measured an annotation overhead of one annotation per 50 lines of code at a cost of one programmer hour per thousand lines of code [13].”
Effective static race detection for Java (2006, background): “…and Subject Descriptors D.2.4 [Software Engineering]: Software/Program Veri.cation Reliability; D.2.5 [Software Engineering]: Testing and Debugging Debugging aids General Terms Experimentation, Reliability Keywords static race detection, Java, synchronization, concurrency, multi-threading 1.”
Ownership types for safe programming: preventing data races and deadlocks (2002, methodology): “• Formal Rules for Type Checking: To simplify the presentation of key ideas behind our approach, this paper formally presents our type system in the context of a core subset of Java called Concurrent Java [7, 22, 23].”
Hybrid dynamic data race detection (2003, positive): “Our paper also presents a formalization of lockset-based and happens-before-based approaches in a common framework, allowing us to prove a folk theorem that happens-before detection reports fewer false positives than lockset-based detection (but can report more false negatives), and to prove…”