Flávio Manuel Fernandes Cruz

Linear Logic and Coordination for Parallel Programming Degree Type: Ph.D. in Computer Science
Advisor(s): Seth Goldstein, Frank Pfenning, Ricardo Rocha
Graduated: May 2016

Abstract:

Parallel programming is known to be difficult to apply, exploit and reason about. Programs written using low level parallel constructs tend to be problematic to understand and debug. Declarative programming is a step towards the right direction because it moves the details of parallelization from the programmer to the runtime system. However, this paradigm leaves the programmer with little opportunities to coordinate the execution of the program, resulting in suboptimal declarative programs. We propose a new declarative programming language, called Linear Meld (LM), that provides a solution to this problem by supporting data-driven dynamic coordination mechanisms that are semantically equivalent to regular computation.

LM is a logic programming language designed for programs that operate on graphs and supports coordination and structured manipulation of mutable state. Coordination is achieved through two mechanisms: (i) coordination facts, which allow the programmer to control how computation is scheduled and how data is laid out, and (ii) thread facts, which allow the programmer to reason about the state of the underlying parallel architecture. The use of coordination allows the programmer to combine the inherent implicit parallelism of LM with a form of declarative explicit parallelism provided by coordination, allowing the development of complex coordinated programs that run faster than regular programs. Furthermore, since coordination is indistinguishable from regular computation, it allows the programmer to reason both about the problem at hand and also about parallel execution.

We have written several graph algorithms, search algorithms and machine learning algorithms in LM. For some programs, we have written informal proofs of correctness to show that programs are easily proven correct. We have also engineered a compiler and runtime system that is able to run LM programs on multi core architectures with decent performance and scalability.

Thesis Committee:
Frank Pfenning (Co-Chair)
Seth Goldstein (Co-Chair)
Ricardo Rocha (Co-Chair, University of Porto)
Umut Acar
Luis Barbosa (University of Minho)
Carlos Guestrin (University of Washington)

Frank Pfenning, Head, Computer Science Department
Andrew W. Moore, Dean, School of Computer Science

Keywords:
Programming Languages, Parallel Programming, Coordination, Linear Logic, Logic Programming, Implementation