Scans in Π-Ware
This project was a case study for Π-Ware, an Embedded Domain-Specific Language (EDSL) for hardware description created by João Paulo Pizani Flor for his master thesis. In this project we wanted see if we could implement and prove properties about scans.
It was supervised by Wouter Swierstra, and i worked together with João Paulo Pizani Flor.
A scan (also known as a parallel prefix sum) takes a sequence of inputs 𝑥1, 𝑥2, … , 𝑥𝑛 and produces the outputs 𝑥1, (𝑥1 ⊕ 𝑥2), …, (𝑥1 ⊕ 𝑥2 ⊕ … ⊕ 𝑥𝑛), where ⊕ is some binary associative operator. Scans are fundamental building blocks for many efficient parallel algorithms including integer addition, sorting and calculation of convex hulls.
We used the proofs of Ralf Hinze in ‘An algebra of scans’ as a basis for our proofs.
The project was quite successful. I was able to extend Π-Ware such that Hinze’s proofs could be mapped quite directly.
Talk
I have given a talk about the project. It was given as part of the Computer Science colloquium and is meant to be accessible for a wide audience.
Report
The project report is is mostly focused on documenting the solutions and the mistakes before those solutions. I assume some knowledge about the background, so i would recommend reading about that first:
- João’s thesis - Π-Ware (pdf). Mainly chapters 3.1, 3.2.1, 3.2.2, 3.3.1 and 3.3.2. Note that some details and names have changed in the meantime.
- Ralf Hinze - An Algebra of Scans (pdf). Up to chapter 4.
Code
The code is publicly available on Github:
It is being merged into the main code base of Π-Ware, so at some point this repository should become obsolete.