Write a Blog >>
PLDI 2020
Mon 15 - Fri 19 June 2020
Thu 18 Jun 2020 14:40 - 15:00 at PLDI Research Papers live stream - Language Design I Chair(s): Adrian Sampson

The Bluespec hardware-description language presents a significantly higher-level view than hardware engineers are used to, exposing a simpler concurrency model that promotes formal proof, without compromising on performance of compiled circuits.
Unfortunately, the cost model of Bluespec has been unclear, with performance details depending on a mix of user hints and opaque static analysis of potential concurrency conflicts within a design.
In this paper we present Koika, a derivative of Bluespec that preserves its desirable properties and yet gives direct control over the \emph{scheduling} decisions that determine performance.
Koika has a novel and deterministic operational semantics that uses dynamic analysis to avoid concurrency anomalies.
Our implementation includes Coq definitions of syntax, semantics, key metatheorems, and a verified compiler to circuits.
We argue that most of the extra circuitry required for dynamic analysis can be eliminated by compile-time BSV-style static analysis.

Thu 18 Jun
Times are displayed in time zone: (GMT-07:00) Pacific Time (US & Canada) change

14:20 - 15:40: PLDI Research Papers - Language Design I at PLDI Research Papers live stream
Chair(s): Adrian SampsonCornell University, USA

YouTube lightning session video

pldi-2020-papers14:20 - 14:40
Benjamin BichselETH Zurich, Switzerland, Maximilian BaaderETH Zurich, Switzerland, Timon GehrETH Zurich, Switzerland, Martin VechevETH Zurich, Switzerland
pldi-2020-papers14:40 - 15:00
Thomas BourgeatMassachusetts Institute of Technology, USA, Clément Pit-ClaudelMassachusetts Institute of Technology, USA, Adam ChlipalaMassachusetts Institute of Technology, ArvindMassachusetts Institute of Technology, USA
pldi-2020-papers15:00 - 15:20
Fabian SchuikiETH Zurich, Switzerland, Andreas KurthETH Zurich, Switzerland, Tobias GrosserETH Zurich, Switzerland, Luca BeniniETH Zurich, Switzerland
Link to publication Pre-print
pldi-2020-papers15:20 - 15:40
Shaopeng ZhuUniversity of Maryland, USA, Shih-Han HungUniversity of Maryland, USA, Shouvanik ChakrabartiUniversity of Maryland, USA, Xiaodi WuUniversity of Maryland, USA