Abstract
A race condition is a situation where two threads manipulate a data structure simultaneously, without synchronization. Race conditions are common errors in multithreaded programming. They often lead to unintended nondeterminism and wrong results. Moreover, they are notoriously hard to diagnose, and attempts to eliminate them can introduce deadlocks. In practice, race conditions and deadlocks are often avoided through prudent programming discipline: protecting each shared data structure with a lock and imposing a partial order on lock acquisitions. In this paper we show that this discipline can be captured (if not completely, to a significant extent) through a set of static rules. We present these rules as a type system for a concurrent, imperative language. Although weaker than a full-blown program-verification calculus, the type system is effective and easy to apply. We emphasize a core, first-order type system focused on race conditions; we also consider extensions with polymorphism, existential types, and a partial order on lock types.
Chapter PDF
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
S. Abramsky, S. Gay, and R. Nagarajan. A type-theoretic approach to deadlockfreedom of asynchronous systems. In Theoretical Aspects of Computer Software, volume 1281 of Lecture Notes in Computer Science, pages 295–320. Springer-Verlag, 1997.
A. Aiken and D. Gay. Barrier inference. In Proceedings of the 25th Symposium on Principles of Programming Languages, pages 243–354, 1998.
T. Amtoft, F. Nielson, and H. R. Nielson. Type and behaviour reconstruction for higher-order concurrent programs. Journal of Functional Programming, 7(3):321–347, 1997.
G. S. Avrunin, U. A. Buy, J. C. Corbett, L. K. Dillon, and J. C. Wileden. Automated analysis of concurrent systems with the constrained expression toolset. IEEE Transactions on Software Engineering, 17(11):1204–1222, 1991.
A. D. Birrell. An introduction to programming with threads. Research Report 35, Digital Equipment Corporation Systems Research Center, 1989.
L. Cardelli. Type systems. Handbook of Computer Science and Engineering, pages 2208–2236, 1997.
A. T. Chamillard, L. A. Clarke, and G. S. Avrunin. An empirical comparison of static concurrency analysis techniques. Technical Report 96-084, Department of Computer Science, University of Massachusetts at Amherst, 1996.
G.-I. Cheng, M. Feng, C. E. Leiserson, K. H. Randall, and A. F. Stark. Detecting data races in Cilk programs that use locks. In Proceedings of the 10th Symposium on Parallel Algorithms and Architectures, pages 298–309, 1998.
C. Colby. Analyzing the communication topology of concurrent programs. In ACM Symposium on Partial Evaluation and Semantics-Based Program Manipulation, pages 202–213, 1995.
J. C. Corbett. Evaluating deadlock detection methods for concurrent software. IEEE Transactions on Software Engineering, 22(3):161–180, 1996.
M. B. Dwyer and L. A. Clarke. Data flow analysis for verifying properties of concurrent programs. Technical Report 94-045, Department of Computer Science, University of Massachusetts at Amherst, 1994.
L. Fajstrup, E. Goubault, and M. Raussen. Detecting deadlocks in concurrent systems. In CONCUR'98: Concurrency Theory, volume 1466 of Lecture Notes in Computer Science. Springer-Verlag, 1998.
P. Godefroid. Model checking for programming languages using VeriSoft. In Proceedings of the 24th Symposium on Principles of Programming Languages, pages 174–186, 1997.
J. Gosling, B. Joy, and G. Steele. The Java Language Specification. Addison-Wesley, 1996.
P. Jouvelot and D. Gifford. Algebraic reconstruction of types and effects. In Proceedings of the 18th Symposium on Principles of Programming Languages, pages 303–310, 1991.
N. Kobayashi. A partially deadlock-free typed process calculus. In Proceedings of the 12th Annual IEEE Symposium on Logic in Computer Science, pages 128–139, 1997.
J. M. Lucassen and D. K. Gifford. Polymorphic effect systems. In Proceedings of the ACM Conference on Lisp and Functional Programming, pages 47–57, 1988.
F. Nielson. Annotated type and effect systems. ACM Computing Surveys, 28(2):344–345, 1996. Invited position statement for the Symposium on Models of Programming Languages and Computation.
H. R. Nielson and F. Nielson. Higher-order concurrent programs with finite communication topology. In Proceedings of the 21st Symposium on Principles of Programming Languages, pages 84–97, 1994.
J. H. Reppy. CML: a higher-order concurrent language. In ACM’ 91 Conference on Programming Language Design and Implementation., pages 293–305, 1991.
S. Savage, M. Burrows, G. Nelson, P. Sobalvarro, and T. E. Anderson. Eraser: A dynamic data race detector for multi-threaded programs. ACM Transactions on Computer Systems, 15(4):391–411, 1997.
N. Sterling. Warlock: A static data race analysis tool. In USENIXWinter Technical Conference, pages 97–106, 1993.
J.-P. Talpin and P. Jouvelot. Polymorphic type, region and effect inference. Journal of Functional Programming, 2(3):245–271, 1992.
M. Tofte and J.-P. Talpin. Implementation of the typed call-by-value lambdacalculus using a stack of regions. In Proceedings of the 21st Symposium on Principles of Programming Languages, pages 188–201, 1994.
M. Tofte and J.-P. Talpin. Region-based memory management. Information and Computation, 132(2):109–176, 1997.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1999 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Flanagan, C., Abadi, M. (1999). Types for Safe Locking. In: Swierstra, S.D. (eds) Programming Languages and Systems. ESOP 1999. Lecture Notes in Computer Science, vol 1576. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-49099-X_7
Download citation
DOI: https://doi.org/10.1007/3-540-49099-X_7
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-65699-9
Online ISBN: 978-3-540-49099-9
eBook Packages: Springer Book Archive