Safe locking for multi-threaded Java with exceptions
| Autor: | Einar Broch Johnsen, Thi Mai Thuong Tran, Olaf Owe, Martin Steffen |
|---|---|
| Rok vydání: | 2012 |
| Předmět: |
Record locking
Java Computer science Readers–writers problem Logic Readers–writer lock 02 engineering and technology Software_PROGRAMMINGTECHNIQUES Re-entrant locks computer.software_genre Type and effect systems Theoretical Computer Science Multi-threading 0202 electrical engineering electronic engineering information engineering Lock convoy Exceptions Non-lexical computer.programming_language Programming language Lock-based concurrency 020207 software engineering Static analysis Java concurrency Giant lock Computational Theory and Mathematics Ticket lock 020201 artificial intelligence & image processing computer Software |
| Zdroj: | The Journal of Logic and Algebraic Programming |
| ISSN: | 1567-8326 |
| DOI: | 10.1016/j.jlap.2011.11.002 |
| Popis: | There are many mechanisms for concurrency control in high-level programming languages. In Java, the original mechanism for concurrency control, based on synchronized blocks, is lexically scoped. For more flexible control, Java 5 introduced non-lexical lock primitives on re-entrant locks.These operators may lead to run-time errors and unwanted behavior; e.g., taking a lock without releasing it, which could lead to a deadlock, or trying to release a lock without owning it. This paper develops a static type and effect system to prevent the mentioned lock errors for a formal, object-oriented calculus which supports non-lexical lock handling and exceptions. Based on an operational semantics, we prove soundness of the effect type analysis. Challenges in the design of the effect type system are dynamic creation of threads, objects, and especially of locks, aliasing of lock references, passing of lock references between threads, and reentrant locks as found in Java. Furthermore, the exception handling mechanism complicates the control-flow and thus the analysis. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|
Full Text from ScienceDirect