|
Journal description
All volumes of the corresponding journal
All issues of the corresponding volume
All articles of the corresponding issues
Details for article 1 of 1 found articles
| Title: |
Correct-by-Construction Concurrency: Using Dependent Types to Verify Implementations of Effectful Resource Usage Protocols |
| Author: |
Brady, Edwin Hammond, Kevin |
| Appeared in: |
Fundamenta informaticae |
| Paging: | Volume 102 (2010) nr. 2 pages 145-176 |
| Year: |
2010-09-24 |
| Contents: |
In the modern, multi-threaded, multi-core programming environment, correctly managing system resources, including locks and shared variables, can be especially difficult and errorprone. A simple mistake, such as forgetting to release a lock, can have major consequences on the correct operation of a program, by, for example, inducing deadlock, often at a time and location that is isolated from the original error. In this paper, we propose a new type-based approach to resource management, based on the use of dependent types to construct a Domain-Specific Embedded Language (DSEL) whose typing rules directly enforce the formal program properties that we require. In this way, we ensure strong static guarantees of correctness-by-construction, without requiring the development of a new special-purpose type system or the associated special-purpose soundness proofs. We also reduce the need for “over-serialisation”, the overly-conservative use of locks that often occurs in manually constructed software, where formal guarantees cannot be exploited. We illustrate our approach by implementing a DSEL for concurrent programming and demonstrate its applicability with reference to an example based on simple bank account transactions. |
| Publisher: |
IOS Press |
| Source file: |
Elektronische Wetenschappelijke Tijdschriften |
Details for article 1 of 1 found articles