Types for mutual exclusion in concurrent programming languages

One of the most difficult parts of writing concurrent programs is working with shared memory. It is difficult to reason about sections of code working on shared memory because of the possibility of interference from other threads of execution. This interference can be prevented by enforcing the mutual exclusion of resources, but guaranteeing this property is itself a difficult problem. One common way of statically enforcing mutual exclusion is through the use of linear type systems. Linear type systems impose a requirement that values designated as "linear" are used exactly once. This property is useful for several memory safety problems, including the enforcement of mutual exclusion of resources. However, linear type systems used in imperative code require a linearization on the order of imperative operations, rewriting code into a declarative style. In practice, this is inconvenient for programs that makes heavy use of mutable data structures. In order to maintain mutual exclusion of memory in an imperative language, rather than having a type system that requires resources to be single-use, we propose a type system that enforces "single-ownership" of resources, that at any given point in time, a resource is only owned by one thread of execution. The goal of this type system is to obtain mutual exclusion (or race-freedom) for a concurrent language that does not require a linearization of imperative operations. In this thesis, we present a novel type system that can perform this memory analysis for an imperative, higher-order, concurrent language. We state and prove results about the safety and soundness of our type system, and we also present an inference algorithm that can be used to check whether an arbitrary program is typable.

Name thesis:degree_name

M.S.

Level thesis:degree_level

Thesis

Discipline thesis:degree_discipline

Computer Science

Grantor

University of Illinois at Urbana-Champaign

Year dc:date

2022

Author dc:creator

• Lee, John J

Contributors dc:contributor

• Gunter, Elsa L

• Formal Verification
• Type Systems
• Concurrent Programming

Statement dc:rights

• Copyright 2022 John J. Lee

Language dc:language

en, eng

Handle dc:identifier

https://hdl.handle.net/2142/117836

OAI record oai:identifier

https://www.ideals.illinois.edu/oai-pmh?verb=GetRecord&metadataPrefix=etdms&identifier=oai%3Awww.ideals.illinois.edu%3A2142%2F117836