Linear Logic and Coordination for Parallel Programming

Flávio Cruz

December 2015


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 co- ordinate 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 multicore architectures with decent performance and scalability.

Bibtex

@PhdThesis{cruz-phd,
  author =  {F. Cruz},
  title =   {{Linear Logic and Coordination for Parallel Programming}},
  school =  {University of Porto / Carnegie Mellon University},
  address = {Portugal / Pittsburgh, Pennsylvania, USA},
  month =   {December},
  year =    {2015},
  type =    {{PhD Thesis}},
}

Download Thesis

PDF file