SPLS online — October 21st (11:00–)

SystemVerilog is a well-known Hardware Description and Verification Language. Many attempts at formalising such languages concentrate of formalising the behaviour of designs at the Register Transaction Level i.e. the signals going across the wire. Hardware design is becoming increasingly commoditised and it might be the case that several components of your design are encrypted bitstreams bought from third-parties. Here we must have trust that the encrypted bitstreams do what they are supposed to.

In the Border Patrol Project we are interested in being able to reason about the structure & behaviour of designs as a whole, regardless of if we can inspect each module down to the individual gates & wires. In this talk I will introduce PicoSystemVerilog (PSV) [0,1] a lambda calculus we are developing that encapsulates various structural aspects of SystemVerilog, and allows us to reason about Design structure. I will show that a PSV Design can capture the essence of a Design's structure, and also enforce substructural properties over data types as defined in the SystemVerilog standard using techniques borrowed from maths-a-magical structured programming. With PSV we hope to establish a foundational formalisation that we can later extend to reason about other structural characteristics and also about a design's behaviour.

[0] This is work in heavy progress and is not incredibly polished.

[1] The name is heavily subject to me being able to think of a much cooler name whose acronym doesn't make me think of PSV Eindhoven.

Python is a popular, dynamic language for data science and scientific computing. To ensure efficiency, significant numerical libraries are implemented in static native languages. However, performance suffers when switching between native and non-native code, especially if data has to be converted between native arrays and Python data structures. As GPU accelerators are increasingly used, this problem becomes particularly acute. Data and control has to be repeatedly transferred between the accelerator and the host.

In this talk, we present DelayRepay, a delayed execution framework for numeric Python programs. It avoids excessive switching and data transfer by using lazy evaluation and kernel fusion. Using DelayRepay, operations on NumPy arrays are executed lazily, allowing multiple calls to accelerator kernels to be fused together dynamically. DelayRepay is available as a drop-in replacement for existing Python libraries. This approach enables significant performance improvement over the state-of-the-art and is invisible to the application programmer. We show that our approach provides an average 24× speedup over NumPy - a 60% increase over the state of the art.

Dependently typed languages such as Coq and Agda can statically guarantee the correctness of our proofs and programs. To provide this guarantee, they restrict users to certain schemes – such as strictly positive datatypes, complete case analysis, and well-founded induction – that are known to be safe. However, these restrictions limit the expressivity of the language and can make programs and proofs hard to write.

In this talk I present Rewriting Type Theory (RTT), a dependently typed language with user-defined higher-order rewrite rules. These rewrite rules can be used to ease reasoning about existing definitions, and to extend the language with new constructs such as quotient types and exceptions. To ensure subject reduction in the presence of rewrite rules, I present a general method to check confluence based on Tait and Martin-Löf's triangle property of parallel reduction. We have implemented rewrite rules as an extension to Agda, and formalized the meta-theoretic properties of RTT using the MetaCoq framework.

The approach of LIFT is to provide high performance high-level programming with code portability. The rewrite system of LIFT systematically transforms high-level algorithmic patterns into low-level high performance OpenCL code with equivalent functionality by applying a set of rewrite rules. To ensure the effectiveness of these rewrite rules, we would like to:

1. Formalise the type constraints of them
2. Prove their correctness

We have encoded the semantics of LIFT in Agda and developed mechanical proofs to the correctness of these rewrite rules. We would like to present our findings in equality reasoning about array/tensor operations with Agda.

C++20 extends the capabilities of generalised constant expressions to include transient dynamic memory allocation; which must be freed before evaluation of the surrounding constant expression.

While interactivity, and other ad-hoc restrictions on constant expressions remain, the opportunity now exists to integrate existing and idiomatic stateful programs within type level calculations.

The C++ standard library is the most basic dependency of a project; and shipped with every compiler. Yet, while compile-time dynamic memory allocation is functional, algorithms and containers from the standard library are not available for use within constant expressions.

We introduce the C'est library: providing a growing subset of common functions and classes from the C++ standard library, applicable within constant expressions. The need for strongly-typed allocation arises, and we introduce emergent idioms to overcome the limitations of transient allocation.

Pervasive memory errors, including uninitialised memory access; using non-owned memory; buffer overflows; and double free errors, are all now capable of capture through compilation errors; rather than runtime errors. While template metaprogramming has been avoided, there is nevertheless a development cost, with the capabilities of the debugger stretched; and memory debuggers now indispensable in the quest even to compile larger programs.

We conclude with a case study involving compile-time verification of the Metamath proof database format, and discuss our ongoing work within the Clang constant expression evaluator.

NVidia's CUDA programming environment provides several options on how to orchestrate the management of host and device memory as well as the transfers between them. This talk gives a brief overview of the options available and it discusses the implications of those choices for generating CUDA code from high-level specifications. Finally, we present some initial performance evaluations based on a full fledged implementation in the Sac compiler sac2c.