Marina Lifshin

dblp:78/1961 · DBLP profile ↗
← Back
1ranked-venue papers
0as first author
0since 2021 · last 2008
—ORCID · none

Domains — the database's venue-derived domains; a paper can count in several

Software engineering, systems software and programming languages · 1

Expertise — from the expertise taxonomy: the topics of the expert's papers under the CCF categories. A weight counts papers with recency: 1 for a paper about the topic, 0.3 when the topic is its context, halved every five years.

Software engineering, system software, and programming languages
1 paper
Programming languages and type systems · 61% Concurrent programming · 39%

Topics — the 4 heaviest of 4, each with the papers that count most for it

TopicWeightPapersLastEvidence papers
Concurrent programming
atomicity
0.112008
Types for atomicity: Static checking and inference for Java · ACM Trans. Program. Lang. Syst. 2008
Programming languages and type systems › type systems › behavioral type systems
atomicity type system
0.112008
Types for atomicity: Static checking and inference for Java · ACM Trans. Program. Lang. Syst. 2008
Programming languages and type systems
type systems
0.112008
Types for atomicity: Static checking and inference for Java · ACM Trans. Program. Lang. Syst. 2008
Concurrent programming › concurrency bug detection
data race detection
0.012008
Types for atomicity: Static checking and inference for Java · ACM Trans. Program. Lang. Syst. 2008

Methods — techniques the papers use, named apart from their topics

type inference · 0.1reduction theory · 0.1
YearPublicationVenuePosition
2008 Types for atomicity: Static checking and inference for Java
abstract
Atomicity is a fundamental correctness property in multithreaded programs. A method is atomic if, for every execution, there is an equivalent serial execution in which the actions of the method are not interleaved with actions of other threads. Atomic methods are amenable to sequential reasoning, which significantly facilitates subsequent analysis and verification. This article presents a type system for specifying and verifying the atomicity of methods in multithreaded Java programs using a synthesis of Lipton's theory of reduction and type systems for race detection. The type system supports guarded, write-guarded, and unguarded fields, as well as thread-local data, parameterized classes and methods, and protected locks. We also present an algorithm for verifying atomicity via type inference. We have applied our type checker and type inference tools to a number of commonly used Java library classes and programs. These tools were able to verify the vast majority of methods in these benchmarks as atomic, indicating that atomicity is a widespread methodology for multithreaded programming. In addition, reported atomicity violations revealed some subtle errors in the synchronization disciplines of these programs.
Cormac Flanagan, Stephen N. Freund, Marina Lifshin, Shaz Qadeer
ACM Trans. Program. Lang. Syst.3