Séminaire LSL - Morten Tychsen Clausen - Rogers: Writing Verified Programs for Computational Storage

Abstract

Computational storage is the idea of pushing computations to a storage device containing data of interest, rather than loading the data onto a host device and then performing the computation. Offloading computations aims to minimize data movement and increase performance by allowing computations to make better use of the hardware found on the storage device. To ensure the correctness of these computations, we define Rogers, a framework for verified computational storage. Rogers consists of three components: - A programming paradigm which separates data management and computations into two distinct domains for easier verification; - A domain-specific language for expressing data placements and invoking computations. This is accompanied by a type checker that validates applications written in the DSL; - A resource manager to provide concurrent memory access for applications on computational storage devices.

Rogers enables storage vendors to market their devices as more trustworthy, service providers to offer computational services without worries of security, and application developers to easily interact with computational storage for increased performance.