META '19: "From Definitional Interpreter ..."
From Definitional Interpreter to Symbolic Executor
Adrian D. Mensing, Hendrik van Antwerpen, Casper Bach Poulsen, and Eelco Visser
(Delft University of Technology, Netherlands)
Symbolic execution is a technique for automatic software validation and verification. New symbolic executors regularly appear for both existing and new languages and such symbolic executors are generally manually (re)implemented each time we want to support a new language. We propose to automatically generate symbolic executors from language definitions, and present a technique for mechanically (but as yet, manually) deriving a symbolic executor from a definitional interpreter. The idea is that language designers define their language as a monadic definitional interpreter, where the monad of the interpreter defines the meaning of branch points. Developing a symbolic executor for a language is a matter of changing the monadic interpretation of branch points. In this paper, we illustrate the technique on a language with recursive functions and pattern matching, and use the derived symbolic executor to automatically generate test cases for definitional interpreters implemented in our defined language.
@InProceedings{META19p11,
author = {Adrian D. Mensing and Hendrik van Antwerpen and Casper Bach Poulsen and Eelco Visser},
title = {From Definitional Interpreter to Symbolic Executor},
booktitle = {Proc.\ META},
publisher = {ACM},
pages = {11--20},
doi = {10.1145/3358502.3361269},
year = {2019},
}
Publisher's Version
Info
META '19: "Squirrel: An Extensible Distributed ..."
Squirrel: An Extensible Distributed Key-Value Store
Kevin De Porre and Elisa Gonzalez Boix
(Vrije Universiteit Brussel, Belgium)
Distributed key-value (KV) stores are a rising alternative to traditional relational databases since they provide a flexible yet simple data model. Recent KV stores use eventual consistency to ensure fast reads and writes as well as high availability. Support for eventual consistency is however still very limited as typically only a handful of replicated data types are provided. Moreover, modern applications maintain various types of data, some of which require strong consistency whereas other require high availability. Implementing such applications remains cumbersome due to the lack of support for data consistency in today's KV stores. In this paper we propose Squirrel, an open implementation of an in-memory distributed KV store. The core idea is to reify distribution through consistency models and protocols. We implement two families of consistency models (strong consistency and strong eventual consistency) and several consistency protocols, including two-phase commit and CRDTs.
@InProceedings{META19p21,
author = {Kevin De Porre and Elisa Gonzalez Boix},
title = {Squirrel: An Extensible Distributed Key-Value Store},
booktitle = {Proc.\ META},
publisher = {ACM},
pages = {21--30},
doi = {10.1145/3358502.3361271},
year = {2019},
}
Publisher's Version
META '19: "Squirrel: An Extensible Distributed ..."
Squirrel: An Extensible Distributed Key-Value Store
Kevin De Porre and Elisa Gonzalez Boix
(Vrije Universiteit Brussel, Belgium)
Distributed key-value (KV) stores are a rising alternative to traditional relational databases since they provide a flexible yet simple data model. Recent KV stores use eventual consistency to ensure fast reads and writes as well as high availability. Support for eventual consistency is however still very limited as typically only a handful of replicated data types are provided. Moreover, modern applications maintain various types of data, some of which require strong consistency whereas other require high availability. Implementing such applications remains cumbersome due to the lack of support for data consistency in today's KV stores. In this paper we propose Squirrel, an open implementation of an in-memory distributed KV store. The core idea is to reify distribution through consistency models and protocols. We implement two families of consistency models (strong consistency and strong eventual consistency) and several consistency protocols, including two-phase commit and CRDTs.
@InProceedings{META19p21,
author = {Kevin De Porre and Elisa Gonzalez Boix},
title = {Squirrel: An Extensible Distributed Key-Value Store},
booktitle = {Proc.\ META},
publisher = {ACM},
pages = {21--30},
doi = {10.1145/3358502.3361271},
year = {2019},
}
Publisher's Version
META '19: "Ambiguous, Informal, and Unsound: ..."
Ambiguous, Informal, and Unsound: Metaprogramming for Naturalness
Toni Mattis, Patrick Rein, and Robert Hirschfeld
(HPI, Germany)
Program code needs to be understood by both machines and programmers. While the goal of executing programs requires the unambiguity of a formal language, programmers use natural language within these formal constraints to explain implemented concepts to each other. This so called naturalness – the property of programs to resemble human communication – motivated many statistical and machine learning (ML) approaches with the goal to improve software engineering activities.
The metaprogramming facilities of most programming environments model the formal elements of a program (meta-objects). If ML is used to support engineering or analysis tasks, complex infrastructure needs to bridge the gap between meta-objects and ML models, changes are not reflected in the ML model, and the mapping from an ML output back into the program’s meta-object domain is laborious.
In the scope of this work, we propose to extend metaprogramming facilities to give tool developers access to the representations of program elements within an exchangeable ML model. We demonstrate the usefulness of this abstraction in two case studies on test prioritization and refactoring. We conclude that aligning ML representations with the program’s formal structure lowers the entry barrier to exploit statistical properties in tool development.
@InProceedings{META19p1,
author = {Toni Mattis and Patrick Rein and Robert Hirschfeld},
title = {Ambiguous, Informal, and Unsound: Metaprogramming for Naturalness},
booktitle = {Proc.\ META},
publisher = {ACM},
pages = {1--10},
doi = {10.1145/3358502.3361270},
year = {2019},
}
Publisher's Version
META '19: "FlashFreeze: Low-Overhead ..."
FlashFreeze: Low-Overhead JavaScript Instrumentation for Function Serialization
Jonathan Van der Cruysse, Lode Hoste, and Wolfgang Van Raemdonck
(Ghent University, Belgium; Nokia Bell Labs, USA)
Object serialization is important to a variety of applications, including session migration and distributed computing. A general JavaScript object serializer must support function serialization as functions are first-class objects. However, JavaScript offers no built-in function serialization and limits custom serializers by exposing no meta operator to query a function’s captured variables. Code instrumentation can expose captured variables but state-of-the-art instrumentation techniques introduce high overheads, vary in supported syntax and/or use complex (de)serialization algorithms.
We introduce FlashFreeze, an instrumentation technique based on capture lists. FlashFreeze achieves a tiny run time overhead: an Octane score reduction of 3% compared to 76% for the state-of-the-art ThingsMigrate tool and 1% for the work-in-progress FSM tool. FlashFreeze supports all self-contained ECMAScript 5 programs except for specific uses of eval, with, and source code inspection. FlashFreeze’s construction gives rise to simple (de)serialization algorithms.
@InProceedings{META19p31,
author = {Jonathan Van der Cruysse and Lode Hoste and Wolfgang Van Raemdonck},
title = {FlashFreeze: Low-Overhead JavaScript Instrumentation for Function Serialization},
booktitle = {Proc.\ META},
publisher = {ACM},
pages = {31--39},
doi = {10.1145/3358502.3361268},
year = {2019},
}
Publisher's Version
META '19: "Ambiguous, Informal, and Unsound: ..."
Ambiguous, Informal, and Unsound: Metaprogramming for Naturalness
Toni Mattis, Patrick Rein, and Robert Hirschfeld
(HPI, Germany)
Program code needs to be understood by both machines and programmers. While the goal of executing programs requires the unambiguity of a formal language, programmers use natural language within these formal constraints to explain implemented concepts to each other. This so called naturalness – the property of programs to resemble human communication – motivated many statistical and machine learning (ML) approaches with the goal to improve software engineering activities.
The metaprogramming facilities of most programming environments model the formal elements of a program (meta-objects). If ML is used to support engineering or analysis tasks, complex infrastructure needs to bridge the gap between meta-objects and ML models, changes are not reflected in the ML model, and the mapping from an ML output back into the program’s meta-object domain is laborious.
In the scope of this work, we propose to extend metaprogramming facilities to give tool developers access to the representations of program elements within an exchangeable ML model. We demonstrate the usefulness of this abstraction in two case studies on test prioritization and refactoring. We conclude that aligning ML representations with the program’s formal structure lowers the entry barrier to exploit statistical properties in tool development.
@InProceedings{META19p1,
author = {Toni Mattis and Patrick Rein and Robert Hirschfeld},
title = {Ambiguous, Informal, and Unsound: Metaprogramming for Naturalness},
booktitle = {Proc.\ META},
publisher = {ACM},
pages = {1--10},
doi = {10.1145/3358502.3361270},
year = {2019},
}
Publisher's Version
META '19: "From Definitional Interpreter ..."
From Definitional Interpreter to Symbolic Executor
Adrian D. Mensing, Hendrik van Antwerpen, Casper Bach Poulsen, and Eelco Visser
(Delft University of Technology, Netherlands)
Symbolic execution is a technique for automatic software validation and verification. New symbolic executors regularly appear for both existing and new languages and such symbolic executors are generally manually (re)implemented each time we want to support a new language. We propose to automatically generate symbolic executors from language definitions, and present a technique for mechanically (but as yet, manually) deriving a symbolic executor from a definitional interpreter. The idea is that language designers define their language as a monadic definitional interpreter, where the monad of the interpreter defines the meaning of branch points. Developing a symbolic executor for a language is a matter of changing the monadic interpretation of branch points. In this paper, we illustrate the technique on a language with recursive functions and pattern matching, and use the derived symbolic executor to automatically generate test cases for definitional interpreters implemented in our defined language.
@InProceedings{META19p11,
author = {Adrian D. Mensing and Hendrik van Antwerpen and Casper Bach Poulsen and Eelco Visser},
title = {From Definitional Interpreter to Symbolic Executor},
booktitle = {Proc.\ META},
publisher = {ACM},
pages = {11--20},
doi = {10.1145/3358502.3361269},
year = {2019},
}
Publisher's Version
Info
META '19: "Ambiguous, Informal, and Unsound: ..."
Ambiguous, Informal, and Unsound: Metaprogramming for Naturalness
Toni Mattis, Patrick Rein, and Robert Hirschfeld
(HPI, Germany)
Program code needs to be understood by both machines and programmers. While the goal of executing programs requires the unambiguity of a formal language, programmers use natural language within these formal constraints to explain implemented concepts to each other. This so called naturalness – the property of programs to resemble human communication – motivated many statistical and machine learning (ML) approaches with the goal to improve software engineering activities.
The metaprogramming facilities of most programming environments model the formal elements of a program (meta-objects). If ML is used to support engineering or analysis tasks, complex infrastructure needs to bridge the gap between meta-objects and ML models, changes are not reflected in the ML model, and the mapping from an ML output back into the program’s meta-object domain is laborious.
In the scope of this work, we propose to extend metaprogramming facilities to give tool developers access to the representations of program elements within an exchangeable ML model. We demonstrate the usefulness of this abstraction in two case studies on test prioritization and refactoring. We conclude that aligning ML representations with the program’s formal structure lowers the entry barrier to exploit statistical properties in tool development.
@InProceedings{META19p1,
author = {Toni Mattis and Patrick Rein and Robert Hirschfeld},
title = {Ambiguous, Informal, and Unsound: Metaprogramming for Naturalness},
booktitle = {Proc.\ META},
publisher = {ACM},
pages = {1--10},
doi = {10.1145/3358502.3361270},
year = {2019},
}
Publisher's Version
META '19: "From Definitional Interpreter ..."
From Definitional Interpreter to Symbolic Executor
Adrian D. Mensing, Hendrik van Antwerpen, Casper Bach Poulsen, and Eelco Visser
(Delft University of Technology, Netherlands)
Symbolic execution is a technique for automatic software validation and verification. New symbolic executors regularly appear for both existing and new languages and such symbolic executors are generally manually (re)implemented each time we want to support a new language. We propose to automatically generate symbolic executors from language definitions, and present a technique for mechanically (but as yet, manually) deriving a symbolic executor from a definitional interpreter. The idea is that language designers define their language as a monadic definitional interpreter, where the monad of the interpreter defines the meaning of branch points. Developing a symbolic executor for a language is a matter of changing the monadic interpretation of branch points. In this paper, we illustrate the technique on a language with recursive functions and pattern matching, and use the derived symbolic executor to automatically generate test cases for definitional interpreters implemented in our defined language.
@InProceedings{META19p11,
author = {Adrian D. Mensing and Hendrik van Antwerpen and Casper Bach Poulsen and Eelco Visser},
title = {From Definitional Interpreter to Symbolic Executor},
booktitle = {Proc.\ META},
publisher = {ACM},
pages = {11--20},
doi = {10.1145/3358502.3361269},
year = {2019},
}
Publisher's Version
Info
META '19: "FlashFreeze: Low-Overhead ..."
FlashFreeze: Low-Overhead JavaScript Instrumentation for Function Serialization
Jonathan Van der Cruysse, Lode Hoste, and Wolfgang Van Raemdonck
(Ghent University, Belgium; Nokia Bell Labs, USA)
Object serialization is important to a variety of applications, including session migration and distributed computing. A general JavaScript object serializer must support function serialization as functions are first-class objects. However, JavaScript offers no built-in function serialization and limits custom serializers by exposing no meta operator to query a function’s captured variables. Code instrumentation can expose captured variables but state-of-the-art instrumentation techniques introduce high overheads, vary in supported syntax and/or use complex (de)serialization algorithms.
We introduce FlashFreeze, an instrumentation technique based on capture lists. FlashFreeze achieves a tiny run time overhead: an Octane score reduction of 3% compared to 76% for the state-of-the-art ThingsMigrate tool and 1% for the work-in-progress FSM tool. FlashFreeze supports all self-contained ECMAScript 5 programs except for specific uses of eval, with, and source code inspection. FlashFreeze’s construction gives rise to simple (de)serialization algorithms.
@InProceedings{META19p31,
author = {Jonathan Van der Cruysse and Lode Hoste and Wolfgang Van Raemdonck},
title = {FlashFreeze: Low-Overhead JavaScript Instrumentation for Function Serialization},
booktitle = {Proc.\ META},
publisher = {ACM},
pages = {31--39},
doi = {10.1145/3358502.3361268},
year = {2019},
}
Publisher's Version
META '19: "FlashFreeze: Low-Overhead ..."
FlashFreeze: Low-Overhead JavaScript Instrumentation for Function Serialization
Jonathan Van der Cruysse, Lode Hoste, and Wolfgang Van Raemdonck
(Ghent University, Belgium; Nokia Bell Labs, USA)
Object serialization is important to a variety of applications, including session migration and distributed computing. A general JavaScript object serializer must support function serialization as functions are first-class objects. However, JavaScript offers no built-in function serialization and limits custom serializers by exposing no meta operator to query a function’s captured variables. Code instrumentation can expose captured variables but state-of-the-art instrumentation techniques introduce high overheads, vary in supported syntax and/or use complex (de)serialization algorithms.
We introduce FlashFreeze, an instrumentation technique based on capture lists. FlashFreeze achieves a tiny run time overhead: an Octane score reduction of 3% compared to 76% for the state-of-the-art ThingsMigrate tool and 1% for the work-in-progress FSM tool. FlashFreeze supports all self-contained ECMAScript 5 programs except for specific uses of eval, with, and source code inspection. FlashFreeze’s construction gives rise to simple (de)serialization algorithms.
@InProceedings{META19p31,
author = {Jonathan Van der Cruysse and Lode Hoste and Wolfgang Van Raemdonck},
title = {FlashFreeze: Low-Overhead JavaScript Instrumentation for Function Serialization},
booktitle = {Proc.\ META},
publisher = {ACM},
pages = {31--39},
doi = {10.1145/3358502.3361268},
year = {2019},
}
Publisher's Version
META '19: "From Definitional Interpreter ..."
From Definitional Interpreter to Symbolic Executor
Adrian D. Mensing, Hendrik van Antwerpen, Casper Bach Poulsen, and Eelco Visser
(Delft University of Technology, Netherlands)
Symbolic execution is a technique for automatic software validation and verification. New symbolic executors regularly appear for both existing and new languages and such symbolic executors are generally manually (re)implemented each time we want to support a new language. We propose to automatically generate symbolic executors from language definitions, and present a technique for mechanically (but as yet, manually) deriving a symbolic executor from a definitional interpreter. The idea is that language designers define their language as a monadic definitional interpreter, where the monad of the interpreter defines the meaning of branch points. Developing a symbolic executor for a language is a matter of changing the monadic interpretation of branch points. In this paper, we illustrate the technique on a language with recursive functions and pattern matching, and use the derived symbolic executor to automatically generate test cases for definitional interpreters implemented in our defined language.
@InProceedings{META19p11,
author = {Adrian D. Mensing and Hendrik van Antwerpen and Casper Bach Poulsen and Eelco Visser},
title = {From Definitional Interpreter to Symbolic Executor},
booktitle = {Proc.\ META},
publisher = {ACM},
pages = {11--20},
doi = {10.1145/3358502.3361269},
year = {2019},
}
Publisher's Version
Info