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