Rogers: Writing Verified Programs for Computational Storage

Computational storage is the idea of pushing computations to the storage device containing the data of interest rather than loading the data onto a host device and then performing the computation. This approach aims to minimize data movement and increase performance by allowing computations that make better use of the hardware found on the storage device.

This approach to data modification is still in its infancy, and as such there are many open research questions regarding the architecture and implementation of such a setup. Some of those questions have been posed by Barbalace & Do [10], of which this thesis focuses on: How to program applications? How to manage shared resources? How to ensure application are safe to execute on the storage device?

This thesis takes a step towards answering the above questions through the following
contributions.
• A programming paradigm which separates data management and computations into two distinct domains. This allows storage providers to control what kind of computations are executed on their devices, while still providing users with the ability to configure the computations to their desire.
• A domain-specific language (DSL) for expressing data placements and invoking computations. This is accompanied by Rogers, a type checker that validates applications written in the DSL. The DSL combines its type system with region-based memory management, enabling Rogers to validate that no buffer overflows occur. The user is thus freed from worrying about the correctness of low-level memory details.
• A resource manager to provide shared memory access to applications on compu-
tational storage devices. Concurrency with respect to SSDs is an often overlooked
topic, so this contribution serves to take a first step toward addressing the topic. The
manager is co-designed alongside the DSL and utilizes a deterministic queue system
to guarantee the absence of deadlocks and eventual access for applications.

The contributions result in storage vendors being able to market their computational storage devices as more trustworthy, service providers being able to offer computational services without worries of security, and application developers having an easy way to interact with computational storage for increased performance.