Types for mutual exclusion in concurrent programming languages

Lee, John J

Permalink

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

Description

Title

Types for mutual exclusion in concurrent programming languages

Author(s)

Lee, John J

Issue Date

2022-12-06

Director of Research (if dissertation) or Advisor (if thesis)

Gunter, Elsa L

Department of Study

Computer Science

Discipline

Computer Science

Degree Granting Institution

University of Illinois at Urbana-Champaign

Degree Name

M.S.

Degree Level

Thesis

Keyword(s)

• Formal Verification
• Type Systems
• Concurrent Programming

Abstract

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.

Graduation Semester

2022-12

Type of Resource

Thesis

Copyright and License Information

Copyright 2022 John J. Lee

Owning Collections