Search

The idea of pushing computation to storage devices has been explored for decades, without widespread adoption so far. The definition of Computational Programs namespaces in NVMe (TP 4091) might be a breakthrough. The proposal defines device-specific programs, that are installed statically, and downloadable programs, offloaded from a host at run-time using eBPF. In this paper, we present the design and implementation of Delilah, the first public description of an actual computational storage device supporting eBPF-based code offload. We conduct experiments to evaluate the overhead of eBPF function execution in Delilah, and to explore design options. This study constitutes a baseline for future work.

Encryption is a special case of conditional loss-less transformation and is, thus, interesting to study from the perspective of reversible computations. In this paper we investigate some of the advantages of implementing encryption algorithms in a reversible language; here exemplified by implementing several symmetric lightweight encryption algorithms in Janus. We not only get both encryption and decryption programs with the same implementation, but also demonstrate how to translate the Janus program to a Vale program, which is then intended to be used to formally show the absence of state information leakage. This shows a way to use reversible programming to increase resilience to some side-channel attacks and give prospects for writing more secure algorithms in the future. Our experience shows that the implementation time is not significantly increased when implementing the algorithms in Janus.

An essential part of many organisations is the ability to provide the users and decision makers with reports on key data based on large amounts data, and these reports should be delivered in a timely manner to stay relevant. To get the desired performance the programs generating these reports are often written in a non-intuitive fashion. For instance, by keeping data in a denormalized form. We have investigated an alternative approach, namely to write the programs as they are operating on the full amount of data and then use automatic incrementalization for achieving acceptable performance.

This paper presents and evaluates a novel second-order operator, named 'redomap', that stems from 'map'-'reduce' compositions in the context of the purely-functional array language Futhark, which is aimed at efficient GPGPU execution. Main contributions are: First, we demonstrate an aggressive fusion technique that is centered on the 'redomap' operator. Second, we present a compilation technique for 'redomap' that efficiently sequentializes the excess parallelism and ensures coalesced access to global memory, even for non-commutative 'reduce' operators. Third, a detailed performance evaluation shows that Futhark's automatically generated code matches or exceeds performance of hand-tuned Thrust code. Our evaluation infrastructure is publicly available and we encourage replication and verification of our results.

With more personal data being stored in the “cloud” every day, privacy is becoming an important topic for public discussion. Private data is potentially quite useful, but cannot be released in its raw form due to privacy concerns. Differential privacy is an emerging field of research aiming to protect the privacy of individuals participating in a database while maximizing its utility. PINQ is a framework for the C# enforcing differential privacy constraints over top of the popular integrated query language, LINQ. Users are able to build complex, differentially-private queries from a few carefully implemented primitives. PINQ data providers are then able to dynamically reject queries which could put private informa- tion at risk. Type systems can statically verify programs for varying degrees of correctness. De- pendent types are a particularly powerful feature of certain type systems which allows types to be predicated on values. Because of this, we believe dependent types are a natural fit for capturing differential privacy metrics. We present a prototype of a differentially-private query language, DPDT, in the dependently-typed, functional programming language Idris. DPDT is loosely modelled on PINQ. However, whereas PINQ verifies privacy constraints dynamically, DPDT is able to do it statically. In addition, DPDT is completely type-safe in all of its relational algebra operations. We outline the benefits and drawbacks to using dependent types for enforcing dif- ferential privacy. Limitations of DPDT in comparison to PINQ are backend support, and expressibility of dynamically terminating algorithms. However, a large number of side-channel attacks that PINQ is unable to stop are impossible in DPDT.

We provide an implementation of session types in Rust and demonstrate how to incorporate session-typed channels in the Servo browser engine to guarantee protocol safety among concurrent, communicating threads. Session types provide a protocol abstraction, expanding on traditional typed communication channels, to ensure communication takes place according to a specified protocol. Existing browser engines are over a decade old and unfit for modern computer architectures, where parallelism and energy efficiency are prioritized over raw power. To take advantage of modern computing platforms Mozilla Research is developing Servo, a next-generation rendering engine. Servo is implemented in Rust, a new systems programming language that provides memory-safety and simple concurrency mechanisms, while retaining the speed of C or C++, all of which is essential to Servo. We present and discuss the overall design of Servo and its internal communication patterns and demonstrate how the design can lead to discrepancies in communication expectations and potentially result in errors. The communication patterns employed in Servo are defined in an ad-hoc manner without any imposed overall structure. The adhoc communication patterns make it difficult to reason about communication flow and it is therefore hard to make assertions concerning safety and deadlock-freedom. To address these issues, we design and implement a session type library in Rust called session-types, and discuss practical use cases through examples and demonstrate how they may be used in a large-scale application. Specifically, we replace parts of Servo’s internal communication infrastructure with session-typed channels, and demonstrate that the use of session types allows us to provide compile-time guarantees, without incurring any significant run-time penalties. We also discuss challenges and drawbacks we discovered when using session-typed communication in a large real-world application. Our work is pu

The skyline operator has recently emerged as an alternative to ranking queries and retrieves a number of potential best options for arbitrary monotone preference functions. The success of this operator in the database community is based on the belief that users benefit from the limited effort required to specify skyline queries with respect to, for instance, ranking. However, while application examples exist and research on efficient computation in a variety of settings abounds, there exists no principled analysis of its benefits and limitations in data retrieval tasks. Our study investigates the degree to which users understand skyline queries, how they specify query parameters and how they interact with skyline results made available in listings or map-based interfaces.

The world of finance faces the computational performance challenge of massively expanding data volumes, extreme response time requirements, and compute-intensive complex (risk) analyses. Simultaneously, new international regulatory rules require considerably more transparency and external auditability of financial institutions, including their software systems. To top it off, increased product variety and customisation necessitates shorter software development cycles and higher development productivity. In this paper, we report about HIPERFIT, a recently etablished strategic research center at the University of Copenhagen that attacks this triple challenge of increased performance, transparency and productivity in the financial sector by a novel integration of financial mathematics, domain-specific language technology, parallel functional programming, and emerging massively parallel hardware. HIPERFIT seeks to contribute to effective high-performance modelling by domain specialists, and to functional programming on highly parallel computer architectures in particular, by pursuing a research trajectory informed by the application domain of finance, but without limiting its research scope, generality, or applicablity, to finance. Research in HIPERFIT draws on and aims at producing new research in its different scientific fields, and it fosters synergies between them to deliver showcases of modern language technology and advanced functional methods with the potential for disruptive impact on an area of increasing societal importance.

This paper demonstrates how relational algebraic programming based on efficient symbolic representations of multisets and operations on them can be applied to the query sublanguage of SQL in a type-safe fashion. In essence, it provides a library for naïve programming with multisets in a generalized SQL-style fashion, but avoids many cases of asymptotically inefficient nested iteration through cross-products.

Binary Decision Diagrams (BDDs) are a data structure used to efficiently represent boolean expressions on canonical form. BDDs are often the core data structure in model checkers. MuDDy is an ML interface (both for Standard ML and Objective Caml) to the BDD package BuDDy that is written in C. This combination of an ML interface to a high-performance C library is surprisingly fruitful. ML allows you to quickly experiment with high-level symbolic algorithms before handing over the grunt work to the C library. I show how, with a relatively little effort, you can make a domain specific language for concurrent finite state-machines embedded in Standard ML and then write various custom model-checking algorithms for this domain specific embedded language (DSEL).

One of the essential features of enterprise resource planning systems is the ability to provide the users and decision makers with reports on how the enterprise is running, and to enable the enterprise to provide the authorities the required legal reports. By their nature these reports needs to operate on large amounts of data and the decision makers need the reports in a timely manner. To achieve acceptable performance of the programs that generates these reports, the data, the full transaction log, the programs operates on is kept in denormalized form. What we propose instead is to write the programs as they are operating on the full amount of data and then use automatic incrementalization for achieving acceptable performance. To study whether automatic incrementalization is practically feasible we introduce the reporting language FunSETL, which is a restricted ML dialect, a compiler for FunSETL that can perform automatic incrementalization, and we have collected a small suite of reporting programs written in FunSETL containing a real life report. We show that using incrementalization on our suite we obtain an asymptotic improvement of a linear factor in the running time compared to the non-incrementalized original programs.

Invited contribution

I denne artikel beskriver vi nogle af de faldgruber ved konstruktionsprojekter, vi har observeret, studerende oftest falder i. Ved at beskrive ofte forekommende problemer er det vores håb, at både vejledere og studerende bedre kan blive opmærksomme på dem og imødekomme dem.