DLS '18: "A Trustworthy Mechanized Formalization ..."
A Trustworthy Mechanized Formalization of R
Martin Bodin, Tomás Diaz, and Éric Tanter
(University of Chile, Chile)
The R programming language is very popular for developing statistical software and data analysis, thanks to rich libraries, concise and expressive syntax, and support for interactive programming. Yet, the semantics of R is fairly complex, contains many subtle corner cases, and is not formally specified. This makes it difficult to reason about R programs. In this work, we develop a big-step operational semantics for R in the form of an interpreter written in the Coq proof assistant. We ensure the trustworthiness of the formalization by introducing a monadic encoding that allows the Coq interpreter, CoqR, to be in direct visual correspondence with the reference R interpreter, GNU R. Additionally, we provide a testing framework that supports systematic comparison of CoqR and GNU R. In its current state, CoqR covers the nucleus of the R language as well as numerous additional features, making it pass a significant number of realistic test cases from the GNU R and FastR projects. To exercise the formal specification, we prove in Coq the preservation of memory invariants in selected parts of the interpreter. This work is an important first step towards a robust environment for formal verification of R programs.
@InProceedings{DLS18p13,
author = {Martin Bodin and Tomás Diaz and Éric Tanter},
title = {A Trustworthy Mechanized Formalization of R},
booktitle = {Proc.\ DLS},
publisher = {ACM},
pages = {13--24},
doi = {10.1145/3276945.3276946},
year = {2018},
}
Publisher's Version
DLS '18: "Self-Contained Development ..."
Self-Contained Development Environments
Guido Chari, Javier Pimás, Jan Vitek, and Olivier Flückiger
(Czech Technical University, Czechia; Palantir Solutions, Argentina; Northeastern University, USA)
Operating systems are traditionally implemented in low- level, performance-oriented programming languages. These languages typically rely on minimal runtime support and provide unfettered access to the underlying hardware. Tra- dition has benefits: developers control the resources that the operating system manages and few performance bottle- necks cannot be overcome with clever feats of programming. On the other hand, this makes operating systems harder to understand and maintain. Furthermore, those languages have few built-in barriers against bugs. This paper is an ex- periment in side-stepping operating systems, and pushing functionality into the runtime of high-level programming languages. The question we try to answer is how much sup- port is needed to run an application written in, say, Smalltalk or Python on bare metal, that is, with no underlying oper- ating system. We present a framework named NopSys that allows this, and we validate it with the implementation of CogNos a Smalltalk virtual machine running on bare x86 hardware. Experimental results suggest that this approach is promising.
@InProceedings{DLS18p76,
author = {Guido Chari and Javier Pimás and Jan Vitek and Olivier Flückiger},
title = {Self-Contained Development Environments},
booktitle = {Proc.\ DLS},
publisher = {ACM},
pages = {76--87},
doi = {10.1145/3276945.3276948},
year = {2018},
}
Publisher's Version
DLS '18: "HorseIR: Bringing Array Programming ..."
HorseIR: Bringing Array Programming Languages Together with Database Query Processing
Hanfeng Chen, Joseph Vinish D'silva, Hongji Chen, Bettina Kemme, and Laurie Hendren
(McGill University, Canada)
Relational database management systems (RDBMS) are operationally similar to a dynamic language processor. They take SQL queries as input, dynamically generate an optimized execution plan, and then execute it. In recent decades, the emergence of in-memory databases with columnar storage, which use array-like storage structures, has shifted the focus on optimizations from the traditional I/O bottleneck to CPU and memory. However, database research so far has primarily focused on CPU cache optimizations. The similarity in the computational characteristics of such database workloads and array programming language optimizations are largely unexplored. We believe that these database implementations can benefit from merging database optimizations with dynamic array-based programming language approaches. Therefore, in this paper, we propose a novel approach to optimize database query execution using a new array-based intermediate representation, HorseIR, that resides between database queries and compiled code. Furthermore, we provide a translator to generate HorseIR from database execution plans and a compiler that optimizes HorseIR and generates efficient code. We compare HorseIR with the MonetDB RDBMS, by testing standard SQL queries, and show how our approach and compiler optimizations improve the runtime of complex queries.
@InProceedings{DLS18p37,
author = {Hanfeng Chen and Joseph Vinish D'silva and Hongji Chen and Bettina Kemme and Laurie Hendren},
title = {HorseIR: Bringing Array Programming Languages Together with Database Query Processing},
booktitle = {Proc.\ DLS},
publisher = {ACM},
pages = {37--49},
doi = {10.1145/3276945.3276951},
year = {2018},
}
Publisher's Version
Info
DLS '18: "Numerical Computing on the ..."
Numerical Computing on the Web: Benchmarking for the Future
David Herrera, Hanfeng Chen, Erick Lavoie, and Laurie Hendren
(McGill University, Canada)
Recent advances in execution environments for JavaScript and WebAssembly that run on a broad range of devices, from workstations and mobile phones to IoT devices, provide new opportunities for portable and web-based numerical computing. Indeed, numerous numerical libraries and applications are emerging on the web, including Tensorflow.js, JSMapReduce, and the NLG Protein Viewer. This paper evaluates the current performance of numerical computing on the web, including both JavaScript and WebAssembly, over a wide range of devices from workstations to IoT devices. We developed a new benchmarking approach, which allowed us to perform centralized benchmarking, including benchmarking on mobile and IoT devices. Using this approach we performed four performance studies using the Ostrich benchmark suite, a collection of numerical programs representing the numerical dwarf categories identified by Colella. We studied the performance evolution of JavaScript, the relative performance of WebAssembly, the performance of server-side Node.js, and a comprehensive performance showdown for a wide range of devices.
@InProceedings{DLS18p88,
author = {David Herrera and Hanfeng Chen and Erick Lavoie and Laurie Hendren},
title = {Numerical Computing on the Web: Benchmarking for the Future},
booktitle = {Proc.\ DLS},
publisher = {ACM},
pages = {88--100},
doi = {10.1145/3276945.3276968},
year = {2018},
}
Publisher's Version
DLS '18: "HorseIR: Bringing Array Programming ..."
HorseIR: Bringing Array Programming Languages Together with Database Query Processing
Hanfeng Chen, Joseph Vinish D'silva, Hongji Chen, Bettina Kemme, and Laurie Hendren
(McGill University, Canada)
Relational database management systems (RDBMS) are operationally similar to a dynamic language processor. They take SQL queries as input, dynamically generate an optimized execution plan, and then execute it. In recent decades, the emergence of in-memory databases with columnar storage, which use array-like storage structures, has shifted the focus on optimizations from the traditional I/O bottleneck to CPU and memory. However, database research so far has primarily focused on CPU cache optimizations. The similarity in the computational characteristics of such database workloads and array programming language optimizations are largely unexplored. We believe that these database implementations can benefit from merging database optimizations with dynamic array-based programming language approaches. Therefore, in this paper, we propose a novel approach to optimize database query execution using a new array-based intermediate representation, HorseIR, that resides between database queries and compiled code. Furthermore, we provide a translator to generate HorseIR from database execution plans and a compiler that optimizes HorseIR and generates efficient code. We compare HorseIR with the MonetDB RDBMS, by testing standard SQL queries, and show how our approach and compiler optimizations improve the runtime of complex queries.
@InProceedings{DLS18p37,
author = {Hanfeng Chen and Joseph Vinish D'silva and Hongji Chen and Bettina Kemme and Laurie Hendren},
title = {HorseIR: Bringing Array Programming Languages Together with Database Query Processing},
booktitle = {Proc.\ DLS},
publisher = {ACM},
pages = {37--49},
doi = {10.1145/3276945.3276951},
year = {2018},
}
Publisher's Version
Info
DLS '18: "A Trustworthy Mechanized Formalization ..."
A Trustworthy Mechanized Formalization of R
Martin Bodin, Tomás Diaz, and Éric Tanter
(University of Chile, Chile)
The R programming language is very popular for developing statistical software and data analysis, thanks to rich libraries, concise and expressive syntax, and support for interactive programming. Yet, the semantics of R is fairly complex, contains many subtle corner cases, and is not formally specified. This makes it difficult to reason about R programs. In this work, we develop a big-step operational semantics for R in the form of an interpreter written in the Coq proof assistant. We ensure the trustworthiness of the formalization by introducing a monadic encoding that allows the Coq interpreter, CoqR, to be in direct visual correspondence with the reference R interpreter, GNU R. Additionally, we provide a testing framework that supports systematic comparison of CoqR and GNU R. In its current state, CoqR covers the nucleus of the R language as well as numerous additional features, making it pass a significant number of realistic test cases from the GNU R and FastR projects. To exercise the formal specification, we prove in Coq the preservation of memory invariants in selected parts of the interpreter. This work is an important first step towards a robust environment for formal verification of R programs.
@InProceedings{DLS18p13,
author = {Martin Bodin and Tomás Diaz and Éric Tanter},
title = {A Trustworthy Mechanized Formalization of R},
booktitle = {Proc.\ DLS},
publisher = {ACM},
pages = {13--24},
doi = {10.1145/3276945.3276946},
year = {2018},
}
Publisher's Version
DLS '18: "HorseIR: Bringing Array Programming ..."
HorseIR: Bringing Array Programming Languages Together with Database Query Processing
Hanfeng Chen, Joseph Vinish D'silva, Hongji Chen, Bettina Kemme, and Laurie Hendren
(McGill University, Canada)
Relational database management systems (RDBMS) are operationally similar to a dynamic language processor. They take SQL queries as input, dynamically generate an optimized execution plan, and then execute it. In recent decades, the emergence of in-memory databases with columnar storage, which use array-like storage structures, has shifted the focus on optimizations from the traditional I/O bottleneck to CPU and memory. However, database research so far has primarily focused on CPU cache optimizations. The similarity in the computational characteristics of such database workloads and array programming language optimizations are largely unexplored. We believe that these database implementations can benefit from merging database optimizations with dynamic array-based programming language approaches. Therefore, in this paper, we propose a novel approach to optimize database query execution using a new array-based intermediate representation, HorseIR, that resides between database queries and compiled code. Furthermore, we provide a translator to generate HorseIR from database execution plans and a compiler that optimizes HorseIR and generates efficient code. We compare HorseIR with the MonetDB RDBMS, by testing standard SQL queries, and show how our approach and compiler optimizations improve the runtime of complex queries.
@InProceedings{DLS18p37,
author = {Hanfeng Chen and Joseph Vinish D'silva and Hongji Chen and Bettina Kemme and Laurie Hendren},
title = {HorseIR: Bringing Array Programming Languages Together with Database Query Processing},
booktitle = {Proc.\ DLS},
publisher = {ACM},
pages = {37--49},
doi = {10.1145/3276945.3276951},
year = {2018},
}
Publisher's Version
Info
DLS '18: "Self-Contained Development ..."
Self-Contained Development Environments
Guido Chari, Javier Pimás, Jan Vitek, and Olivier Flückiger
(Czech Technical University, Czechia; Palantir Solutions, Argentina; Northeastern University, USA)
Operating systems are traditionally implemented in low- level, performance-oriented programming languages. These languages typically rely on minimal runtime support and provide unfettered access to the underlying hardware. Tra- dition has benefits: developers control the resources that the operating system manages and few performance bottle- necks cannot be overcome with clever feats of programming. On the other hand, this makes operating systems harder to understand and maintain. Furthermore, those languages have few built-in barriers against bugs. This paper is an ex- periment in side-stepping operating systems, and pushing functionality into the runtime of high-level programming languages. The question we try to answer is how much sup- port is needed to run an application written in, say, Smalltalk or Python on bare metal, that is, with no underlying oper- ating system. We present a framework named NopSys that allows this, and we validate it with the implementation of CogNos a Smalltalk virtual machine running on bare x86 hardware. Experimental results suggest that this approach is promising.
@InProceedings{DLS18p76,
author = {Guido Chari and Javier Pimás and Jan Vitek and Olivier Flückiger},
title = {Self-Contained Development Environments},
booktitle = {Proc.\ DLS},
publisher = {ACM},
pages = {76--87},
doi = {10.1145/3276945.3276948},
year = {2018},
}
Publisher's Version
DLS '18: "The Behavior of Gradual Types: ..."
The Behavior of Gradual Types: A User Study
Preston Tunnell Wilson, Ben Greenman, Justin Pombrio, and Shriram Krishnamurthi
(Brown University, USA; Northeastern University, USA)
There are several different gradual typing semantics, reflecting different trade-offs between performance and type soundness guarantees. Notably absent, however, are any data on which of these semantics developers actually prefer.
We begin to rectify this shortcoming by surveying professional developers, computer science students, and Mechanical Turk workers on their preferences between three gradual typing semantics. These semantics reflect important points in the design space, corresponding to the behaviors of Typed Racket, TypeScript, and Reticulated Python. Our most important finding is that our respondents prefer a runtime semantics that fully enforces statically declared types.
@InProceedings{DLS18p1,
author = {Preston Tunnell Wilson and Ben Greenman and Justin Pombrio and Shriram Krishnamurthi},
title = {The Behavior of Gradual Types: A User Study},
booktitle = {Proc.\ DLS},
publisher = {ACM},
pages = {1--12},
doi = {10.1145/3276945.3276947},
year = {2018},
}
Publisher's Version
DLS '18: "Query-Based Object-Oriented ..."
Query-Based Object-Oriented Programming: A Declarative Web of Objects
Yoav Seginer, Theo Vosse, Gil Harari, and Uri Kolodny
(cdl-lang.org, Netherlands; cdl-lang.org, Israel)
We present a declarative, object-oriented language in which queries play a central role. Queries are used not only to access data, but also to refer to the application’s object members and as a means of program control. The language is fully declarative, with queries and other pure functions defining the relations between the attributes of different objects. A rule-base-like write operation allows state to be updated. Control is achieved by queries selecting the class variants (mixin classes) which are active in each object. The dynamic activation and deactivation of declarative mixin classes allows decomposition of functionality into small reusable classes.
The programming style in the language is functional and reactive, with function applications defining object members. Queries are one type of function, which also serves as the glue which puts these functions together, providing them with their input. Since queries describe declaratively what they return, they leave it to the system to implement the how of getting it. Combining this with an organization around objects makes the language highly suitable for complex interactive applications driven by large amounts of data from multiple sources.
Our implementation of the language includes a strong display component. It can be seen as a conceptual extension of HTML and CSS in a way which replaces the need for the JavaScript imperative component in web applications. The work described here is not restricted, however, to front-end development and can be applied elsewhere as well.
@InProceedings{DLS18p64,
author = {Yoav Seginer and Theo Vosse and Gil Harari and Uri Kolodny},
title = {Query-Based Object-Oriented Programming: A Declarative Web of Objects},
booktitle = {Proc.\ DLS},
publisher = {ACM},
pages = {64--75},
doi = {10.1145/3276945.3276949},
year = {2018},
}
Publisher's Version
DLS '18: "HorseIR: Bringing Array Programming ..."
HorseIR: Bringing Array Programming Languages Together with Database Query Processing
Hanfeng Chen, Joseph Vinish D'silva, Hongji Chen, Bettina Kemme, and Laurie Hendren
(McGill University, Canada)
Relational database management systems (RDBMS) are operationally similar to a dynamic language processor. They take SQL queries as input, dynamically generate an optimized execution plan, and then execute it. In recent decades, the emergence of in-memory databases with columnar storage, which use array-like storage structures, has shifted the focus on optimizations from the traditional I/O bottleneck to CPU and memory. However, database research so far has primarily focused on CPU cache optimizations. The similarity in the computational characteristics of such database workloads and array programming language optimizations are largely unexplored. We believe that these database implementations can benefit from merging database optimizations with dynamic array-based programming language approaches. Therefore, in this paper, we propose a novel approach to optimize database query execution using a new array-based intermediate representation, HorseIR, that resides between database queries and compiled code. Furthermore, we provide a translator to generate HorseIR from database execution plans and a compiler that optimizes HorseIR and generates efficient code. We compare HorseIR with the MonetDB RDBMS, by testing standard SQL queries, and show how our approach and compiler optimizations improve the runtime of complex queries.
@InProceedings{DLS18p37,
author = {Hanfeng Chen and Joseph Vinish D'silva and Hongji Chen and Bettina Kemme and Laurie Hendren},
title = {HorseIR: Bringing Array Programming Languages Together with Database Query Processing},
booktitle = {Proc.\ DLS},
publisher = {ACM},
pages = {37--49},
doi = {10.1145/3276945.3276951},
year = {2018},
}
Publisher's Version
Info
DLS '18: "Numerical Computing on the ..."
Numerical Computing on the Web: Benchmarking for the Future
David Herrera, Hanfeng Chen, Erick Lavoie, and Laurie Hendren
(McGill University, Canada)
Recent advances in execution environments for JavaScript and WebAssembly that run on a broad range of devices, from workstations and mobile phones to IoT devices, provide new opportunities for portable and web-based numerical computing. Indeed, numerous numerical libraries and applications are emerging on the web, including Tensorflow.js, JSMapReduce, and the NLG Protein Viewer. This paper evaluates the current performance of numerical computing on the web, including both JavaScript and WebAssembly, over a wide range of devices from workstations to IoT devices. We developed a new benchmarking approach, which allowed us to perform centralized benchmarking, including benchmarking on mobile and IoT devices. Using this approach we performed four performance studies using the Ostrich benchmark suite, a collection of numerical programs representing the numerical dwarf categories identified by Colella. We studied the performance evolution of JavaScript, the relative performance of WebAssembly, the performance of server-side Node.js, and a comprehensive performance showdown for a wide range of devices.
@InProceedings{DLS18p88,
author = {David Herrera and Hanfeng Chen and Erick Lavoie and Laurie Hendren},
title = {Numerical Computing on the Web: Benchmarking for the Future},
booktitle = {Proc.\ DLS},
publisher = {ACM},
pages = {88--100},
doi = {10.1145/3276945.3276968},
year = {2018},
}
Publisher's Version
DLS '18: "Numerical Computing on the ..."
Numerical Computing on the Web: Benchmarking for the Future
David Herrera, Hanfeng Chen, Erick Lavoie, and Laurie Hendren
(McGill University, Canada)
Recent advances in execution environments for JavaScript and WebAssembly that run on a broad range of devices, from workstations and mobile phones to IoT devices, provide new opportunities for portable and web-based numerical computing. Indeed, numerous numerical libraries and applications are emerging on the web, including Tensorflow.js, JSMapReduce, and the NLG Protein Viewer. This paper evaluates the current performance of numerical computing on the web, including both JavaScript and WebAssembly, over a wide range of devices from workstations to IoT devices. We developed a new benchmarking approach, which allowed us to perform centralized benchmarking, including benchmarking on mobile and IoT devices. Using this approach we performed four performance studies using the Ostrich benchmark suite, a collection of numerical programs representing the numerical dwarf categories identified by Colella. We studied the performance evolution of JavaScript, the relative performance of WebAssembly, the performance of server-side Node.js, and a comprehensive performance showdown for a wide range of devices.
@InProceedings{DLS18p88,
author = {David Herrera and Hanfeng Chen and Erick Lavoie and Laurie Hendren},
title = {Numerical Computing on the Web: Benchmarking for the Future},
booktitle = {Proc.\ DLS},
publisher = {ACM},
pages = {88--100},
doi = {10.1145/3276945.3276968},
year = {2018},
}
Publisher's Version
DLS '18: "HorseIR: Bringing Array Programming ..."
HorseIR: Bringing Array Programming Languages Together with Database Query Processing
Hanfeng Chen, Joseph Vinish D'silva, Hongji Chen, Bettina Kemme, and Laurie Hendren
(McGill University, Canada)
Relational database management systems (RDBMS) are operationally similar to a dynamic language processor. They take SQL queries as input, dynamically generate an optimized execution plan, and then execute it. In recent decades, the emergence of in-memory databases with columnar storage, which use array-like storage structures, has shifted the focus on optimizations from the traditional I/O bottleneck to CPU and memory. However, database research so far has primarily focused on CPU cache optimizations. The similarity in the computational characteristics of such database workloads and array programming language optimizations are largely unexplored. We believe that these database implementations can benefit from merging database optimizations with dynamic array-based programming language approaches. Therefore, in this paper, we propose a novel approach to optimize database query execution using a new array-based intermediate representation, HorseIR, that resides between database queries and compiled code. Furthermore, we provide a translator to generate HorseIR from database execution plans and a compiler that optimizes HorseIR and generates efficient code. We compare HorseIR with the MonetDB RDBMS, by testing standard SQL queries, and show how our approach and compiler optimizations improve the runtime of complex queries.
@InProceedings{DLS18p37,
author = {Hanfeng Chen and Joseph Vinish D'silva and Hongji Chen and Bettina Kemme and Laurie Hendren},
title = {HorseIR: Bringing Array Programming Languages Together with Database Query Processing},
booktitle = {Proc.\ DLS},
publisher = {ACM},
pages = {37--49},
doi = {10.1145/3276945.3276951},
year = {2018},
}
Publisher's Version
Info
DLS '18: "Query-Based Object-Oriented ..."
Query-Based Object-Oriented Programming: A Declarative Web of Objects
Yoav Seginer, Theo Vosse, Gil Harari, and Uri Kolodny
(cdl-lang.org, Netherlands; cdl-lang.org, Israel)
We present a declarative, object-oriented language in which queries play a central role. Queries are used not only to access data, but also to refer to the application’s object members and as a means of program control. The language is fully declarative, with queries and other pure functions defining the relations between the attributes of different objects. A rule-base-like write operation allows state to be updated. Control is achieved by queries selecting the class variants (mixin classes) which are active in each object. The dynamic activation and deactivation of declarative mixin classes allows decomposition of functionality into small reusable classes.
The programming style in the language is functional and reactive, with function applications defining object members. Queries are one type of function, which also serves as the glue which puts these functions together, providing them with their input. Since queries describe declaratively what they return, they leave it to the system to implement the how of getting it. Combining this with an organization around objects makes the language highly suitable for complex interactive applications driven by large amounts of data from multiple sources.
Our implementation of the language includes a strong display component. It can be seen as a conceptual extension of HTML and CSS in a way which replaces the need for the JavaScript imperative component in web applications. The work described here is not restricted, however, to front-end development and can be applied elsewhere as well.
@InProceedings{DLS18p64,
author = {Yoav Seginer and Theo Vosse and Gil Harari and Uri Kolodny},
title = {Query-Based Object-Oriented Programming: A Declarative Web of Objects},
booktitle = {Proc.\ DLS},
publisher = {ACM},
pages = {64--75},
doi = {10.1145/3276945.3276949},
year = {2018},
}
Publisher's Version
DLS '18: "The Behavior of Gradual Types: ..."
The Behavior of Gradual Types: A User Study
Preston Tunnell Wilson, Ben Greenman, Justin Pombrio, and Shriram Krishnamurthi
(Brown University, USA; Northeastern University, USA)
There are several different gradual typing semantics, reflecting different trade-offs between performance and type soundness guarantees. Notably absent, however, are any data on which of these semantics developers actually prefer.
We begin to rectify this shortcoming by surveying professional developers, computer science students, and Mechanical Turk workers on their preferences between three gradual typing semantics. These semantics reflect important points in the design space, corresponding to the behaviors of Typed Racket, TypeScript, and Reticulated Python. Our most important finding is that our respondents prefer a runtime semantics that fully enforces statically declared types.
@InProceedings{DLS18p1,
author = {Preston Tunnell Wilson and Ben Greenman and Justin Pombrio and Shriram Krishnamurthi},
title = {The Behavior of Gradual Types: A User Study},
booktitle = {Proc.\ DLS},
publisher = {ACM},
pages = {1--12},
doi = {10.1145/3276945.3276947},
year = {2018},
}
Publisher's Version
DLS '18: "Numerical Computing on the ..."
Numerical Computing on the Web: Benchmarking for the Future
David Herrera, Hanfeng Chen, Erick Lavoie, and Laurie Hendren
(McGill University, Canada)
Recent advances in execution environments for JavaScript and WebAssembly that run on a broad range of devices, from workstations and mobile phones to IoT devices, provide new opportunities for portable and web-based numerical computing. Indeed, numerous numerical libraries and applications are emerging on the web, including Tensorflow.js, JSMapReduce, and the NLG Protein Viewer. This paper evaluates the current performance of numerical computing on the web, including both JavaScript and WebAssembly, over a wide range of devices from workstations to IoT devices. We developed a new benchmarking approach, which allowed us to perform centralized benchmarking, including benchmarking on mobile and IoT devices. Using this approach we performed four performance studies using the Ostrich benchmark suite, a collection of numerical programs representing the numerical dwarf categories identified by Colella. We studied the performance evolution of JavaScript, the relative performance of WebAssembly, the performance of server-side Node.js, and a comprehensive performance showdown for a wide range of devices.
@InProceedings{DLS18p88,
author = {David Herrera and Hanfeng Chen and Erick Lavoie and Laurie Hendren},
title = {Numerical Computing on the Web: Benchmarking for the Future},
booktitle = {Proc.\ DLS},
publisher = {ACM},
pages = {88--100},
doi = {10.1145/3276945.3276968},
year = {2018},
}
Publisher's Version
DLS '18: "Log++ Logging for a Cloud-Native ..."
Log++ Logging for a Cloud-Native World
Mark Marron
(Microsoft Research, USA)
Logging is a fundamental part of the software development and deployment lifecycle but logging support is often provided as an afterthought via limited library APIs or third-party modules. Given the critical nature of logging in modern cloud, mobile, and IoT development workflows, the unique needs of the APIs involved, and the opportunities for optimization using semantic knowledge, we argue logging should be included as a central part of the language and runtime designs. This paper presents a rethinking of the logger for modern cloud-native workflows.
Based on a set of design principles for modern logging we build a logging system, that supports near zero-cost for disabled log statements, low cost lazy-copying for enabled log statements, selective persistence of logging output, unified control of logging output across different libraries, and DevOps integration for use with modern cloud-based deployments. To evaluate these concepts we implemented the Log++ logger for Node.js hosted JavaScript applications.
@InProceedings{DLS18p25,
author = {Mark Marron},
title = {Log++ Logging for a Cloud-Native World},
booktitle = {Proc.\ DLS},
publisher = {ACM},
pages = {25--36},
doi = {10.1145/3276945.3276952},
year = {2018},
}
Publisher's Version
Info
DLS '18: "Self-Contained Development ..."
Self-Contained Development Environments
Guido Chari, Javier Pimás, Jan Vitek, and Olivier Flückiger
(Czech Technical University, Czechia; Palantir Solutions, Argentina; Northeastern University, USA)
Operating systems are traditionally implemented in low- level, performance-oriented programming languages. These languages typically rely on minimal runtime support and provide unfettered access to the underlying hardware. Tra- dition has benefits: developers control the resources that the operating system manages and few performance bottle- necks cannot be overcome with clever feats of programming. On the other hand, this makes operating systems harder to understand and maintain. Furthermore, those languages have few built-in barriers against bugs. This paper is an ex- periment in side-stepping operating systems, and pushing functionality into the runtime of high-level programming languages. The question we try to answer is how much sup- port is needed to run an application written in, say, Smalltalk or Python on bare metal, that is, with no underlying oper- ating system. We present a framework named NopSys that allows this, and we validate it with the implementation of CogNos a Smalltalk virtual machine running on bare x86 hardware. Experimental results suggest that this approach is promising.
@InProceedings{DLS18p76,
author = {Guido Chari and Javier Pimás and Jan Vitek and Olivier Flückiger},
title = {Self-Contained Development Environments},
booktitle = {Proc.\ DLS},
publisher = {ACM},
pages = {76--87},
doi = {10.1145/3276945.3276948},
year = {2018},
}
Publisher's Version
DLS '18: "The Behavior of Gradual Types: ..."
The Behavior of Gradual Types: A User Study
Preston Tunnell Wilson, Ben Greenman, Justin Pombrio, and Shriram Krishnamurthi
(Brown University, USA; Northeastern University, USA)
There are several different gradual typing semantics, reflecting different trade-offs between performance and type soundness guarantees. Notably absent, however, are any data on which of these semantics developers actually prefer.
We begin to rectify this shortcoming by surveying professional developers, computer science students, and Mechanical Turk workers on their preferences between three gradual typing semantics. These semantics reflect important points in the design space, corresponding to the behaviors of Typed Racket, TypeScript, and Reticulated Python. Our most important finding is that our respondents prefer a runtime semantics that fully enforces statically declared types.
@InProceedings{DLS18p1,
author = {Preston Tunnell Wilson and Ben Greenman and Justin Pombrio and Shriram Krishnamurthi},
title = {The Behavior of Gradual Types: A User Study},
booktitle = {Proc.\ DLS},
publisher = {ACM},
pages = {1--12},
doi = {10.1145/3276945.3276947},
year = {2018},
}
Publisher's Version
DLS '18: "Query-Based Object-Oriented ..."
Query-Based Object-Oriented Programming: A Declarative Web of Objects
Yoav Seginer, Theo Vosse, Gil Harari, and Uri Kolodny
(cdl-lang.org, Netherlands; cdl-lang.org, Israel)
We present a declarative, object-oriented language in which queries play a central role. Queries are used not only to access data, but also to refer to the application’s object members and as a means of program control. The language is fully declarative, with queries and other pure functions defining the relations between the attributes of different objects. A rule-base-like write operation allows state to be updated. Control is achieved by queries selecting the class variants (mixin classes) which are active in each object. The dynamic activation and deactivation of declarative mixin classes allows decomposition of functionality into small reusable classes.
The programming style in the language is functional and reactive, with function applications defining object members. Queries are one type of function, which also serves as the glue which puts these functions together, providing them with their input. Since queries describe declaratively what they return, they leave it to the system to implement the how of getting it. Combining this with an organization around objects makes the language highly suitable for complex interactive applications driven by large amounts of data from multiple sources.
Our implementation of the language includes a strong display component. It can be seen as a conceptual extension of HTML and CSS in a way which replaces the need for the JavaScript imperative component in web applications. The work described here is not restricted, however, to front-end development and can be applied elsewhere as well.
@InProceedings{DLS18p64,
author = {Yoav Seginer and Theo Vosse and Gil Harari and Uri Kolodny},
title = {Query-Based Object-Oriented Programming: A Declarative Web of Objects},
booktitle = {Proc.\ DLS},
publisher = {ACM},
pages = {64--75},
doi = {10.1145/3276945.3276949},
year = {2018},
}
Publisher's Version
DLS '18: "JavaScript AOT Compilation ..."
JavaScript AOT Compilation
Manuel Serrano
(Inria, France; University of Côte d'Azur, France)
Static compilation, a.k.a., ahead-of-time (AOT) compilation, is an alternative approach to JIT compilation that can combine good speed and lightweight memory footprint, and that can accommodate read-only memory constraints that are imposed by some devices and some operating systems. Unfortunately the highly dynamic nature of JavaScript makes it hard to compile statically and all existing AOT compilers have either gave up on good performance or full language support. We have designed and implemented an AOT compiler that aims at satisfying both. It supports full unrestricted ECMAScript 5.1 plus many ECMAScript 2017 features and the majority of benchmarks are within 50
@InProceedings{DLS18p50,
author = {Manuel Serrano},
title = {JavaScript AOT Compilation},
booktitle = {Proc.\ DLS},
publisher = {ACM},
pages = {50--63},
doi = {10.1145/3276945.3276950},
year = {2018},
}
Publisher's Version
DLS '18: "A Trustworthy Mechanized Formalization ..."
A Trustworthy Mechanized Formalization of R
Martin Bodin, Tomás Diaz, and Éric Tanter
(University of Chile, Chile)
The R programming language is very popular for developing statistical software and data analysis, thanks to rich libraries, concise and expressive syntax, and support for interactive programming. Yet, the semantics of R is fairly complex, contains many subtle corner cases, and is not formally specified. This makes it difficult to reason about R programs. In this work, we develop a big-step operational semantics for R in the form of an interpreter written in the Coq proof assistant. We ensure the trustworthiness of the formalization by introducing a monadic encoding that allows the Coq interpreter, CoqR, to be in direct visual correspondence with the reference R interpreter, GNU R. Additionally, we provide a testing framework that supports systematic comparison of CoqR and GNU R. In its current state, CoqR covers the nucleus of the R language as well as numerous additional features, making it pass a significant number of realistic test cases from the GNU R and FastR projects. To exercise the formal specification, we prove in Coq the preservation of memory invariants in selected parts of the interpreter. This work is an important first step towards a robust environment for formal verification of R programs.
@InProceedings{DLS18p13,
author = {Martin Bodin and Tomás Diaz and Éric Tanter},
title = {A Trustworthy Mechanized Formalization of R},
booktitle = {Proc.\ DLS},
publisher = {ACM},
pages = {13--24},
doi = {10.1145/3276945.3276946},
year = {2018},
}
Publisher's Version
DLS '18: "The Behavior of Gradual Types: ..."
The Behavior of Gradual Types: A User Study
Preston Tunnell Wilson, Ben Greenman, Justin Pombrio, and Shriram Krishnamurthi
(Brown University, USA; Northeastern University, USA)
There are several different gradual typing semantics, reflecting different trade-offs between performance and type soundness guarantees. Notably absent, however, are any data on which of these semantics developers actually prefer.
We begin to rectify this shortcoming by surveying professional developers, computer science students, and Mechanical Turk workers on their preferences between three gradual typing semantics. These semantics reflect important points in the design space, corresponding to the behaviors of Typed Racket, TypeScript, and Reticulated Python. Our most important finding is that our respondents prefer a runtime semantics that fully enforces statically declared types.
@InProceedings{DLS18p1,
author = {Preston Tunnell Wilson and Ben Greenman and Justin Pombrio and Shriram Krishnamurthi},
title = {The Behavior of Gradual Types: A User Study},
booktitle = {Proc.\ DLS},
publisher = {ACM},
pages = {1--12},
doi = {10.1145/3276945.3276947},
year = {2018},
}
Publisher's Version
DLS '18: "Self-Contained Development ..."
Self-Contained Development Environments
Guido Chari, Javier Pimás, Jan Vitek, and Olivier Flückiger
(Czech Technical University, Czechia; Palantir Solutions, Argentina; Northeastern University, USA)
Operating systems are traditionally implemented in low- level, performance-oriented programming languages. These languages typically rely on minimal runtime support and provide unfettered access to the underlying hardware. Tra- dition has benefits: developers control the resources that the operating system manages and few performance bottle- necks cannot be overcome with clever feats of programming. On the other hand, this makes operating systems harder to understand and maintain. Furthermore, those languages have few built-in barriers against bugs. This paper is an ex- periment in side-stepping operating systems, and pushing functionality into the runtime of high-level programming languages. The question we try to answer is how much sup- port is needed to run an application written in, say, Smalltalk or Python on bare metal, that is, with no underlying oper- ating system. We present a framework named NopSys that allows this, and we validate it with the implementation of CogNos a Smalltalk virtual machine running on bare x86 hardware. Experimental results suggest that this approach is promising.
@InProceedings{DLS18p76,
author = {Guido Chari and Javier Pimás and Jan Vitek and Olivier Flückiger},
title = {Self-Contained Development Environments},
booktitle = {Proc.\ DLS},
publisher = {ACM},
pages = {76--87},
doi = {10.1145/3276945.3276948},
year = {2018},
}
Publisher's Version
DLS '18: "Query-Based Object-Oriented ..."
Query-Based Object-Oriented Programming: A Declarative Web of Objects
Yoav Seginer, Theo Vosse, Gil Harari, and Uri Kolodny
(cdl-lang.org, Netherlands; cdl-lang.org, Israel)
We present a declarative, object-oriented language in which queries play a central role. Queries are used not only to access data, but also to refer to the application’s object members and as a means of program control. The language is fully declarative, with queries and other pure functions defining the relations between the attributes of different objects. A rule-base-like write operation allows state to be updated. Control is achieved by queries selecting the class variants (mixin classes) which are active in each object. The dynamic activation and deactivation of declarative mixin classes allows decomposition of functionality into small reusable classes.
The programming style in the language is functional and reactive, with function applications defining object members. Queries are one type of function, which also serves as the glue which puts these functions together, providing them with their input. Since queries describe declaratively what they return, they leave it to the system to implement the how of getting it. Combining this with an organization around objects makes the language highly suitable for complex interactive applications driven by large amounts of data from multiple sources.
Our implementation of the language includes a strong display component. It can be seen as a conceptual extension of HTML and CSS in a way which replaces the need for the JavaScript imperative component in web applications. The work described here is not restricted, however, to front-end development and can be applied elsewhere as well.
@InProceedings{DLS18p64,
author = {Yoav Seginer and Theo Vosse and Gil Harari and Uri Kolodny},
title = {Query-Based Object-Oriented Programming: A Declarative Web of Objects},
booktitle = {Proc.\ DLS},
publisher = {ACM},
pages = {64--75},
doi = {10.1145/3276945.3276949},
year = {2018},
}
Publisher's Version