Premium
Type‐safe concurrent resource sharing
Author(s) -
Wittie Lea,
Lockhart Jonathan
Publication year - 2010
Publication title -
concurrency and computation: practice and experience
Language(s) - English
Resource type - Journals
SCImago Journal Rank - 0.309
H-Index - 67
eISSN - 1532-0634
pISSN - 1532-0626
DOI - 10.1002/cpe.1642
Subject(s) - computer science , shared resource , soundness , deadlock , distributed computing , shared memory , set (abstract data type) , resource (disambiguation) , concurrency control , access control , software , lock (firearm) , programming language , operating system , computer network , engineering , mechanical engineering , database transaction
Concurrent systems often have many processes sharing a common set of resources, both memory regions and hardware devices. Among the many challenges in producing safe concurrent software are single access, atomic transactions, starvation, and deadlock. Locks are frequently used to provide single access to shared resources, but do not guarantee safe usage. This paper extends the previous work on linear, singleton, and arithmetic types and linear memory primitives. Our contributions are capabilities for shared resources, and locks to control these capabilities in provably safe ways. We present formalized locks in a lambda calculus along with the soundness properties of preservation and progress. The type system described here prevents data races. The formalized locks have also been implemented in a C‐like language and used in a network device driver. Copyright © 2010 John Wiley & Sons, Ltd.