• The development of distributed systems requires developers to balance the need for consistency, availability, and partition tolerance. The recently proposed Global Sequence Protocol (GSP) provides an abstract, high-level programming model for asynchronous commands between client and server, which provides a foundation for implementations as well as consistency guarantees. In order to enable offline availability, GSP allows a client to read its own writes even when the client is offline. However, this model can give rise to consistency anomalies that are difficult to debug. In this paper we propose a new consistency protocol, the observable atomic consistency protocol (OACP). OACP enables a principled relaxation of consistency to achieve better performance in certain scenarios. OACP combines the advantages of mergeable data types, specifically, convergent replicated data types (CvRDTs), and reliable total order broadcast (RTOB) to provide on-demand strong consistency, avoiding the anomalies of GSP and related protocols. We implement OACP using Akka Cluster, a state-of-the-art actor framework used in popular, large-scale web applications. The paper also presents an experimental comparison of GSP and OACP. Our evaluation shows that OACP is able to provide lower latency and higher throughput than GSP in several benchmarks.
  • LaCasa is a type system and programming model to enforce the object capability discipline in Scala, and to provide affine types. One important application of LaCasa's type system is software isolation of concurrent processes. Isolation is important for several reasons including security and data-race freedom. Moreover, LaCasa's affine references enable efficient, by-reference message passing while guaranteeing a "deep-copy" semantics. This deep-copy semantics enables programmers to seamlessly port concurrent programs running on a single machine to distributed programs running on large-scale clusters of machines. This paper presents an integration of LaCasa with actors in Scala, specifically, the Akka actor-based middleware, one of the most widely-used actor systems in industry. The goal of this integration is to statically ensure the isolation of Akka actors. Importantly, we present the results of an empirical study investigating the effort required to use LaCasa's type system in existing open-source Akka-based systems and applications.
  • Functional programming typically emphasizes programming with first-class functions and immutable data. Immutable data types enable fault tolerance in distributed systems, and ensure process isolation in message-passing concurrency, among other applications. However, beyond the distinction between reassignable and non-reassignable fields, Scala's type system does not have a built-in notion of immutability for type definitions. As a result, immutability is "by-convention" in Scala, and statistics about the use of immutability in real-world Scala code are non-existent. This paper reports on the results of an empirical study on the use of immutability in several medium-to-large Scala open-source code bases, including Scala's standard library and the Akka actor framework. The study investigates both shallow and deep immutability, two widely-used forms of immutability in Scala. Perhaps most interestingly, for type definitions determined to be mutable, explanations are provided for why neither the shallow nor the deep immutability property holds; in turn, these explanations are aggregated into statistics in order to determine the most common reasons for why type definitions are mutable rather than immutable.
  • Aliasing is a known source of challenges in the context of imperative object-oriented languages, which have led to important advances in type systems for aliasing control. However, their large-scale adoption has turned out to be a surprisingly difficult challenge. While new language designs show promise, they do not address the need of aliasing control in existing languages. This paper presents a new approach to isolation and uniqueness in an existing, widely-used language, Scala. The approach is unique in the way it addresses some of the most important obstacles to the adoption of type system extensions for aliasing control. First, adaptation of existing code requires only a minimal set of annotations. Only a single bit of information is required per class. Surprisingly, the paper shows that this information can be provided by the object-capability discipline, widely-used in program security. We formalize our approach as a type system and prove key soundness theorems. The type system is implemented for the full Scala language, providing, for the first time, a sound integration with Scala's local type inference. Finally, we empirically evaluate the conformity of existing Scala open-source code on a corpus of over 75,000 LOC.
  • Programming systems incorporating aspects of functional programming, e.g., higher-order functions, are becoming increasingly popular for large-scale distributed programming. New frameworks such as Apache Spark leverage functional techniques to provide high-level, declarative APIs for in-memory data analytics, often outperforming traditional "big data" frameworks like Hadoop MapReduce. However, widely-used programming models remain rather ad-hoc; aspects such as implementation trade-offs, static typing, and semantics are not yet well-understood. We present a new asynchronous programming model that has at its core several principles facilitating functional processing of distributed data. The emphasis of our model is on simplicity, performance, and expressiveness. The primary means of communication is by passing functions (closures) to distributed, immutable data. To ensure safe and efficient distribution of closures, our model leverages both syntactic and type-based restrictions. We report on a prototype implementation in Scala. Finally, we present preliminary experimental results evaluating the performance impact of a static, type-based optimization of serialization.
  • Responsive Web Design (RWD) enables web applications to adapt to the characteristics of different devices such as screen size which is important for mobile browsing. Today, the only W3C standard to support this adaptability is CSS media queries. However, using media queries it is impossible to create applications in a modular way, because responsive elements then always depend on the global context. Hence, responsive elements can only be reused if the global context is exactly the same, severely limiting their reusability. This makes it extremely challenging to develop large responsive applications, because the lack of true modularity makes certain requirement changes either impossible or expensive to realize. In this paper we extend RWD to also include responsive modules, i.e., modules that adapt their design based on their local context independently of the global context. We present the ELQ project which implements our approach. ELQ is a novel implementation of so-called element queries which generalize media queries. Importantly, our design conforms to existing web specifications, enabling adoption on a large scale. ELQ is designed to be heavily extensible using plugins. Experimental results show speed-ups of the core algorithms of up to 37x compared to previous approaches.
  • Languages like F#, C#, and recently also Scala, provide "Async" programming models which aim to make asynchronous programming easier by avoiding an inversion of control that is inherent in callback-based programming models. This paper presents a novel approach to integrate the Async model with observable streams of the Reactive Extensions model. Reactive Extensions are best-known from the .NET platform, and widely-used implementations of its programming model exist also for Java, Ruby, and other languages. This paper contributes a formalization of the unified "Reactive Async" model in the context of an object-based core calculus. Our formal model captures the essence of the protocol of asynchronous observables using a heap evolution property. We prove a subject reduction theorem; the theorem implies that reduction preserves the heap evolution property. Thus, for well-typed programs our calculus ensures the protocol of asynchronous observables.