This article demonstrates how a powerful and expressive abstraction from concurrency theory plays a dual rôle as a programming tool for concurrent applications and as a foundation for their verification. This abstraction—monads of resumptions expressed using monad transformers—is cheap: it is easy to understand, easy to implement, and easy to reason about. We illustrate the expressiveness of the resumption monad with the construction of an exemplary multitasking operating system kernel with process forking, preemption, message passing, and synchronization constructs in the pure functional programming language Haskell. Because resumption computations are stream-like structures, reasoning about this kernel may be posed as reasoning about streams, a problem which is well-understood. And, as an example, this article illustrates how a liveness property—fairness—is proven and especially how the resumption-monadic structure promotes such verifications.
Search
Reviews
[Write a review of this article]
Find related articles from these CiteULike users
