A graded Monad for deadlock-free concurrency (functional pearl)
Published version
Peer-reviewed
Repository URI
Repository DOI
Change log
Authors
Ivaškovic, A
Mycroft, Alan https://orcid.org/0000-0001-7013-8572
Abstract
We present a new type-oriented framework for writing shared memory multithreaded programs that the Haskell type system guarantees are deadlock-free. The implementation wraps all concurrent computation inside a graded monad and assumes a total order is defined between locks. The grades within the type of such a computation specify which locks it acquires and releases. This information is drawn from an algebra that ensures that types can, in principle, be inferred in polynomial time.
Description
Keywords
4904 Pure Mathematics, 49 Mathematical Sciences
Journal Title
Haskell 2020 - Proceedings of the 13th ACM SIGPLAN International Symposium on Haskell, co-located with ICFP 2020
Conference Name
ICFP '20: ACM SIGPLAN International Conference on Functional Programming
Journal ISSN
Volume Title
Publisher
ACM
Publisher DOI
Rights
All rights reserved
Sponsorship
Trinity College, Cambridge