6th ACM SIGPLAN Scala Symposium 2015 (SCALA 2015)

Frontmatter

Concurrency and Distribution

SnapQueue: Lock-Free Queue with Constant Time Snapshots
Aleksandar Prokopec
(EPFL, Switzerland)
We introduce SnapQueues - concurrent, lock-free queues with a linearizable, lock-free global-state transition operation. This transition operation can atomically switch between arbitrary SnapQueue states, and is used by enqueue, dequeue, snapshot and concatenation operations. We show that implementing these operations efficiently depends on the persistent data structure at the core of the SnapQueue. This immutable support data structure is an interchangeable kernel of the SnapQueue, and drives its performance characteristics. The design allows reasoning about concurrent operation running time in a functional way, absent from concurrency considerations. We present a support data structure that enables O(1) queue operations, O(1) snapshot and O(log n) atomic concurrent concatenation. We show that the SnapQueue enqueue operation achieves up to 25% higher performance, while the dequeue operation has performance identical to standard lock-free concurrent queues.

@InProceedings{SCALA15p1, author = {Aleksandar Prokopec}, title = {SnapQueue: Lock-Free Queue with Constant Time Snapshots}, booktitle = {Proc.\ SCALA}, publisher = {ACM}, pages = {1--12}, doi = {}, year = {2015}, }

Distributed Programming in Scala with APGAS
Philippe Suter, Olivier Tardieu, and Josh Milthorpe
(IBM Research, USA)
APGAS (Asynchronous Partitioned Global Address Space) is a model for concurrent and distributed programming, known primarily as the foundation of the X10 programming language. In this paper, we present an implementation of this model as an embedded domain-specific language for Scala. We illustrate common usage patterns and contrast with alternative approaches available to Scala programmers. In particular, using two distributed algorithms as examples, we illustrate how APGAS-style programs compare to idiomatic Akka implementations. We demonstrate the use of APGAS places and tasks, distributed termination, and distributed objects.

@InProceedings{SCALA15p13, author = {Philippe Suter and Olivier Tardieu and Josh Milthorpe}, title = {Distributed Programming in Scala with APGAS}, booktitle = {Proc.\ SCALA}, publisher = {ACM}, pages = {13--17}, doi = {}, year = {2015}, }

Types and Verification

Counter-Example Complete Verification for Higher-Order Functions
Nicolas Voirol, Etienne Kneuss, and Viktor Kuncak
(EPFL, Switzerland)
We present a verification procedure for pure higher-order functional Scala programs with parametric types. We show that our procedure is sound for proofs, as well as sound and complete for counter-examples. The procedure reduces the analysis of higher-order programs to checking satisfiability of a sequence of quantifier-free formulas over theories such as algebraic data types, integer linear arithmetic, and uninterpreted function symbols, thus enabling the use of efficient satisfiability modulo theory (SMT) solvers. Our solution supports arbitrary function types and arbitrarily nested anonymous functions (which can be stored in data structures, passed as arguments, returned, and applied). Among the contributions of this work is supporting even those cases when anonymous functions cannot be statically traced back to their definition, ensuring completeness of the approach for finding counter-examples. We provide a proof of soundness and counter-example completeness for our system as well as initial evaluation in the Leon verifier.

@InProceedings{SCALA15p18, author = {Nicolas Voirol and Etienne Kneuss and Viktor Kuncak}, title = {Counter-Example Complete Verification for Higher-Order Functions}, booktitle = {Proc.\ SCALA}, publisher = {ACM}, pages = {18--29}, doi = {}, year = {2015}, }

Referential Integrity with Scala Types
Patrick Prémont
(BoldRadius Solutions, Canada)
Referential integrity constraints are critical elements of relational data models, and have found widespread use in industry. However, their benefits in terms of data integrity do not fully extend to program correctness. Constraint violations are identified at run-time and must then be handled appropriately by programs. We show how Scala can be used to build data models and programs where referential integrity is enforced at compile-time. Scala’s type system, with its variance annotations and path-dependent types, is especially suited to express these constraints and proofs in a natural manner. We also explore potential compiler improvements that could enhance support for type-checked referential integrity.

@InProceedings{SCALA15p30, author = {Patrick Prémont}, title = {Referential Integrity with Scala Types}, booktitle = {Proc.\ SCALA}, publisher = {ACM}, pages = {30--34}, doi = {}, year = {2015}, }

Sound Reasoning about Integral Data Types with a Reusable SMT Solver Interface
Régis Blanc and Viktor Kuncak
(EPFL, Switzerland)
We extend the Leon verification system for Scala with support for bit-vector reasoning, thus addressing one of its fundamental soundness limitation with respect to the treatment of integers primitives. We leverage significant progresses recently achieved in SMT solving by developing a solver-independent interface to easily configure the back-end of Leon. Our interface is based on the emerging SMT-LIB standard for SMT solvers, and we release a Scala library offering full support for the latest version of the standard. We use the standard BigInt Scala library to represent mathematical integers, whereas we correctly model Int as 32-bit integers. We ensure safety of arithmetic by checking for division by zero and correctly modeling division and modulo. We conclude with a performance comparison between the sound representation of Ints and the cleaner abstract representation using mathematical integers, and discuss the trade-off involved.

@InProceedings{SCALA15p35, author = {Régis Blanc and Viktor Kuncak}, title = {Sound Reasoning about Integral Data Types with a Reusable SMT Solver Interface}, booktitle = {Proc.\ SCALA}, publisher = {ACM}, pages = {35--40}, doi = {}, year = {2015}, }

Generative Programming

Fold-Based Fusion as a Library: A Generative Programming Pearl
Manohar Jonnalagedda and Sandro Stucki
(EPFL, Switzerland)
Fusion is a program optimisation technique commonly implemented using special-purpose compiler support. In this paper, we present an alternative approach, implementing fold-based fusion as a standalone library. We use staging to compose operations on folds; the operations are partially evaluated away, yielding code that does not construct unnecessary intermediate data structures. The technique extends to partitioning and grouping of collections.

@InProceedings{SCALA15p41, author = {Manohar Jonnalagedda and Sandro Stucki}, title = {Fold-Based Fusion as a Library: A Generative Programming Pearl}, booktitle = {Proc.\ SCALA}, publisher = {ACM}, pages = {41--50}, doi = {}, year = {2015}, }

ESPeciaL: An Embedded Systems Programming Language
Christopher Métrailler and Pierre-André Mudry
(University of Applied Sciences Western Switzerland, Switzerland)
The advent of off-the-shelf programmable embedded systems such as Arduino enables people with little programming skills to interact with the real-world using sensors and actuators. In this paper, we propose a novel approach aimed at simplifying the programming of embedded systems based on the dataflow paradigm. Named ESPeciaL, this programming framework removes the need of low-level programming in C/C++, as the application is written by connecting blocks that produce and consume data. Thus, an embedded application can be described in terms of ready-to-use blocks that correspond to the various micro-controller peripherals and to program function (multiplexers, logic gates, etc.). The user application itself is written as an embedded Scala DSL. From that code, the ESPeciaL compiler then generates the corresponding C++ code which can be tailored - using different back-ends - to match different embedded systems or a QEMU-based simulation environment. To demonstrate the validity of the approach, we present a typical embedded systems application implemented using ESPeciaL

@InProceedings{SCALA15p51, author = {Christopher Métrailler and Pierre-André Mudry}, title = {ESPeciaL: An Embedded Systems Programming Language}, booktitle = {Proc.\ SCALA}, publisher = {ACM}, pages = {51--55}, doi = {}, year = {2015}, }

proc time: 0.71