Skip to content

Research at St Andrews

Correct-by-Construction Concurrency: Using Dependent Types to Verify Implementations of Effectful Resource Usage Protocols

Research output: Contribution to journalArticle

DOI

Abstract

In the modern, multi-threaded, multi-core programming environment, correctly managing system resources, including locks and shared variables, can be especially difficult and error-prone. 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.

Close

Details

Original languageEnglish
Pages (from-to)145-176
Number of pages32
JournalFundamenta Informaticae
Volume102
Issue number2
DOIs
StatePublished - 2010

    Research areas

  • CALCULUS

Discover related content
Find related publications, people, projects and more using interactive charts.

View graph of relations

Related by author

  1. Resource-Safe Systems Programming with Embedded Domain Specific Languages

    Brady, E. C. & Hammond, K. 2012 Practical Aspects of Declarative Languages: 14th International Symposium, PADL 2012, Philadelphia, PA, USA, January 23-24, 2012. Proceedings. Russo, C. & Zhou, N-F. (eds.). Springer, Vol. 7149, p. 242-257 16 p. (Lecture Notes in Computer Science)

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

  2. Scrapping your inefficient engine: using partial evaluation to improve domain-specific language implementation

    Brady, E. C. & Hammond, K. 2010 ICFP '10: Proceedings of the 15th ACM SIGPLAN international conference on Functional programming. ACM, p. 297-308 12 p.

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

  3. Lightweight Invariants with Full Dependent Types

    Brady, E. C., Herrmann, C. A. & Hammond, K. 2008 Trends in Functional Programming. Intellect Books

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

  4. Constructing Correct Circuits: Verification of Functional Aspects of Hardware Specifications with Dependent Types

    Brady, E. C., McKinna, J. H. & Hammond, K. 2008 Trends in Functional Programming. Intellect Books, Vol. 8, p. 159-176

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

Related by journal

  1. On the Diversity of Orderings on Strings

    Martin, U. H. M. 1995 In : Fundamenta Informaticae. 24, 1-2, p. 25-46

    Research output: Contribution to journalArticle

ID: 4509319