BCTCS 2021

Regular Talk
Functional Programming Semantics Language Theory

Resolving data flow dependencies of concurrent programs with a graded monad

Finnbar Keating

on  Mon, 16:00 ! Live for  30min

In concurrent programs that interact with memory, it is important to know that variables are read from and written to in the correct order to prevent race conditions or inconsistent data. To this end, we introduce a graded monad for identifying the exact memory locations read and written by a given function. With this we can replace Haskell’s IO monad with a variant indexed by a representation of the operations performed. This new information allows us to identify data-flow dependencies between functions at the type-level - that is, if one function reads a memory cell that is written to by another function we might wish to evaluate the latter before the former or vice-versa depending on the context. With these dependencies known at compile-time, we then provide a function that establishes the correct order of execution for these program parts at compile-time with respect to their data-flow dependencies. This compile-time sort even allows us to identify functions that can be run in parallel, and can skip evaluation of code that relies on state that has not changed. We also prevent compilation in the presence of two errors: (1) race conditions via multiple functions writing to the same memory cell, and (2) dependency loops from functions writing to cells that other functions read from.

 Overview  Program