14 Search Results for "Richards, Gregor"


Document
Artifact
Blame for Null (Artifact)

Authors: Abel Nieto, Marianna Rapoport, Gregor Richards, and Ondřej Lhoták

Published in: DARTS, Volume 6, Issue 2, Special Issue of the 34th European Conference on Object-Oriented Programming (ECOOP 2020)


Abstract
This artifact is a companion to the paper "Blame for Null", where we formalize multiple calculi to reason about the interoperability between languages where nullability is explicit and those where nullability is implicit. Our main result is a theorem that states that nullability errors can always be blamed on terms with less-precise typing; that is, terms typed as implicitly nullable. We summarize our result with the slogan explicitly nullable programs can't be blamed. The artifact consists of a mechanized Coq proof of the results presented in the paper.

Cite as

Abel Nieto, Marianna Rapoport, Gregor Richards, and Ondřej Lhoták. Blame for Null (Artifact). In Special Issue of the 34th European Conference on Object-Oriented Programming (ECOOP 2020). Dagstuhl Artifacts Series (DARTS), Volume 6, Issue 2, pp. 10:1-10:2, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2020)


Copy BibTex To Clipboard

@Article{nieto_et_al:DARTS.6.2.10,
  author =	{Nieto, Abel and Rapoport, Marianna and Richards, Gregor and Lhot\'{a}k, Ond\v{r}ej},
  title =	{{Blame for Null (Artifact)}},
  pages =	{10:1--10:2},
  journal =	{Dagstuhl Artifacts Series},
  ISSN =	{2509-8195},
  year =	{2020},
  volume =	{6},
  number =	{2},
  editor =	{Nieto, Abel and Rapoport, Marianna and Richards, Gregor and Lhot\'{a}k, Ond\v{r}ej},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DARTS.6.2.10},
  URN =		{urn:nbn:de:0030-drops-132070},
  doi =		{10.4230/DARTS.6.2.10},
  annote =	{Keywords: nullability, type systems, blame calculus, gradual typing}
}
Document
Blame for Null

Authors: Abel Nieto, Marianna Rapoport, Gregor Richards, and Ondřej Lhoták

Published in: LIPIcs, Volume 166, 34th European Conference on Object-Oriented Programming (ECOOP 2020)


Abstract
Multiple modern programming languages, including Kotlin, Scala, Swift, and C#, have type systems where nullability is explicitly specified in the types. All of the above also need to interoperate with languages where types remain implicitly nullable, like Java. This leads to runtime errors that can manifest in subtle ways. In this paper, we show how to reason about the presence and provenance of such nullability errors using the concept of blame from gradual typing. Specifically, we introduce a calculus, λ_null, where some terms are typed as implicitly nullable and others as explicitly nullable. Just like in the original blame calculus of Wadler and Findler, interactions between both kinds of terms are mediated by casts with attached blame labels, which indicate the origin of errors. On top of λ_null, we then create a second calculus, λ_null^s, which closely models the interoperability between languages with implicit nullability and languages with explicit nullability, such as Java and Scala. Our main result is a theorem that states that nullability errors in λ_null^s can always be blamed on terms with less-precise typing; that is, terms typed as implicitly nullable. By analogy, this would mean that NullPointerExceptions in combined Java/Scala programs are always the result of unsoundness in the Java type system. We summarize our result with the slogan explicitly nullable programs can't be blamed. All our results are formalized in the Coq proof assistant.

Cite as

Abel Nieto, Marianna Rapoport, Gregor Richards, and Ondřej Lhoták. Blame for Null. In 34th European Conference on Object-Oriented Programming (ECOOP 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 166, pp. 3:1-3:28, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2020)


Copy BibTex To Clipboard

@InProceedings{nieto_et_al:LIPIcs.ECOOP.2020.3,
  author =	{Nieto, Abel and Rapoport, Marianna and Richards, Gregor and Lhot\'{a}k, Ond\v{r}ej},
  title =	{{Blame for Null}},
  booktitle =	{34th European Conference on Object-Oriented Programming (ECOOP 2020)},
  pages =	{3:1--3:28},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-154-2},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{166},
  editor =	{Hirschfeld, Robert and Pape, Tobias},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2020.3},
  URN =		{urn:nbn:de:0030-drops-131606},
  doi =		{10.4230/LIPIcs.ECOOP.2020.3},
  annote =	{Keywords: nullability, type systems, blame calculus, gradual typing}
}
Document
Artifact
Reasoning About Foreign Function Interfaces Without Modelling the Foreign Language (Artifact)

Authors: Alexi Turcotte, Ellen Arteca, and Gregor Richards

Published in: DARTS, Volume 5, Issue 2, Special Issue of the 33rd European Conference on Object-Oriented Programming (ECOOP 2019)


Abstract
There are two components to this artifact. First, a we provide a mechanization of the formalization in the paper, as well as mechanized proofs of the main results from the paper. Second, we provide a full implementation of Poseidon Lua, the language implemented in the paper. Instructions for all components of the artifact are included this document.

Cite as

Alexi Turcotte, Ellen Arteca, and Gregor Richards. Reasoning About Foreign Function Interfaces Without Modelling the Foreign Language (Artifact). In Special Issue of the 33rd European Conference on Object-Oriented Programming (ECOOP 2019). Dagstuhl Artifacts Series (DARTS), Volume 5, Issue 2, pp. 9:1-9:2, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2019)


Copy BibTex To Clipboard

@Article{turcotte_et_al:DARTS.5.2.9,
  author =	{Turcotte, Alexi and Arteca, Ellen and Richards, Gregor},
  title =	{{Reasoning About Foreign Function Interfaces Without Modelling the Foreign Language}},
  pages =	{9:1--9:2},
  journal =	{Dagstuhl Artifacts Series},
  ISSN =	{2509-8195},
  year =	{2019},
  volume =	{5},
  number =	{2},
  editor =	{Turcotte, Alexi and Arteca, Ellen and Richards, Gregor},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DARTS.5.2.9},
  URN =		{urn:nbn:de:0030-drops-107863},
  doi =		{10.4230/DARTS.5.2.9},
  annote =	{Keywords: Language design, Language interoperation, Formal semantics}
}
Document
The Dynamic Practice and Static Theory of Gradual Typing

Authors: Michael Greenberg

Published in: LIPIcs, Volume 136, 3rd Summit on Advances in Programming Languages (SNAPL 2019)


Abstract
We can tease apart the research on gradual types into two `lineages': a pragmatic, implementation-oriented dynamic-first lineage and a formal, type-theoretic, static-first lineage. The dynamic-first lineage’s focus is on taming particular idioms - `pre-existing conditions' in untyped programming languages. The static-first lineage’s focus is on interoperation and individual type system features, rather than the collection of features found in any particular language. Both appear in programming languages research under the name "gradual typing", and they are in active conversation with each other. What are these two lineages? What challenges and opportunities await the static-first lineage? What progress has been made so far?

Cite as

Michael Greenberg. The Dynamic Practice and Static Theory of Gradual Typing. In 3rd Summit on Advances in Programming Languages (SNAPL 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 136, pp. 6:1-6:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)


Copy BibTex To Clipboard

@InProceedings{greenberg:LIPIcs.SNAPL.2019.6,
  author =	{Greenberg, Michael},
  title =	{{The Dynamic Practice and Static Theory of Gradual Typing}},
  booktitle =	{3rd Summit on Advances in Programming Languages (SNAPL 2019)},
  pages =	{6:1--6:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-113-9},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{136},
  editor =	{Lerner, Benjamin S. and Bod{\'\i}k, Rastislav and Krishnamurthi, Shriram},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SNAPL.2019.6},
  URN =		{urn:nbn:de:0030-drops-105495},
  doi =		{10.4230/LIPIcs.SNAPL.2019.6},
  annote =	{Keywords: dynamic typing, gradual typing, static typing, implementation, theory, challenge problems}
}
Document
Scopes and Frames Improve Meta-Interpreter Specialization

Authors: Vlad Vergu, Andrew Tolmach, and Eelco Visser

Published in: LIPIcs, Volume 134, 33rd European Conference on Object-Oriented Programming (ECOOP 2019)


Abstract
DynSem is a domain-specific language for concise specification of the dynamic semantics of programming languages, aimed at rapid experimentation and evolution of language designs. To maintain a short definition-to-execution cycle, DynSem specifications are meta-interpreted. Meta-interpretation introduces runtime overhead that is difficult to remove by using interpreter optimization frameworks such as the Truffle/Graal Java tools; previous work has shown order-of-magnitude improvements from applying Truffle/Graal to a meta-interpreter, but this is still far slower than what can be achieved with a language-specific interpreter. In this paper, we show how specifying the meta-interpreter using scope graphs, which encapsulate static name binding and resolution information, produces much better optimization results from Truffle/Graal. Furthermore, we identify that JIT compilation is hindered by large numbers of calls between small polymorphic rules and we introduce rule cloning to derive larger monomorphic rules at run time as a countermeasure. Our contributions improve the performance of DynSem-derived interpreters to within an order of magnitude of a handwritten language-specific interpreter.

Cite as

Vlad Vergu, Andrew Tolmach, and Eelco Visser. Scopes and Frames Improve Meta-Interpreter Specialization. In 33rd European Conference on Object-Oriented Programming (ECOOP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 134, pp. 4:1-4:30, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)


Copy BibTex To Clipboard

@InProceedings{vergu_et_al:LIPIcs.ECOOP.2019.4,
  author =	{Vergu, Vlad and Tolmach, Andrew and Visser, Eelco},
  title =	{{Scopes and Frames Improve Meta-Interpreter Specialization}},
  booktitle =	{33rd European Conference on Object-Oriented Programming (ECOOP 2019)},
  pages =	{4:1--4:30},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-111-5},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{134},
  editor =	{Donaldson, Alastair F.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2019.4},
  URN =		{urn:nbn:de:0030-drops-107969},
  doi =		{10.4230/LIPIcs.ECOOP.2019.4},
  annote =	{Keywords: Definitional interpreters, partial evaluation}
}
Document
Deep Static Modeling of invokedynamic

Authors: George Fourtounis and Yannis Smaragdakis

Published in: LIPIcs, Volume 134, 33rd European Conference on Object-Oriented Programming (ECOOP 2019)


Abstract
Java 7 introduced programmable dynamic linking in the form of the invokedynamic framework. Static analysis of code containing programmable dynamic linking has often been cited as a significant source of unsoundness in the analysis of Java programs. For example, Java lambdas, introduced in Java 8, are a very popular feature, which is, however, resistant to static analysis, since it mixes invokedynamic with dynamic code generation. These techniques invalidate static analysis assumptions: programmable linking breaks reasoning about method resolution while dynamically generated code is, by definition, not available statically. In this paper, we show that a static analysis can predictively model uses of invokedynamic while also cooperating with extra rules to handle the runtime code generation of lambdas. Our approach plugs into an existing static analysis and helps eliminate all unsoundness in the handling of lambdas (including associated features such as method references) and generic invokedynamic uses. We evaluate our technique on a benchmark suite of our own and on third-party benchmarks, uncovering all code previously unreachable due to unsoundness, highly efficiently.

Cite as

George Fourtounis and Yannis Smaragdakis. Deep Static Modeling of invokedynamic. In 33rd European Conference on Object-Oriented Programming (ECOOP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 134, pp. 15:1-15:28, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)


Copy BibTex To Clipboard

@InProceedings{fourtounis_et_al:LIPIcs.ECOOP.2019.15,
  author =	{Fourtounis, George and Smaragdakis, Yannis},
  title =	{{Deep Static Modeling of invokedynamic}},
  booktitle =	{33rd European Conference on Object-Oriented Programming (ECOOP 2019)},
  pages =	{15:1--15:28},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-111-5},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{134},
  editor =	{Donaldson, Alastair F.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2019.15},
  URN =		{urn:nbn:de:0030-drops-108076},
  doi =		{10.4230/LIPIcs.ECOOP.2019.15},
  annote =	{Keywords: static analysis, invokedynamic}
}
Document
Transient Typechecks Are (Almost) Free

Authors: Richard Roberts, Stefan Marr, Michael Homer, and James Noble

Published in: LIPIcs, Volume 134, 33rd European Conference on Object-Oriented Programming (ECOOP 2019)


Abstract
Transient gradual typing imposes run-time type tests that typically cause a linear slowdown. This performance impact discourages the use of type annotations because adding types to a program makes the program slower. A virtual machine can employ standard just-in-time optimizations to reduce the overhead of transient checks to near zero. These optimizations can give gradually-typed languages performance comparable to state-of-the-art dynamic languages, so programmers can add types to their code without affecting their programs' performance.

Cite as

Richard Roberts, Stefan Marr, Michael Homer, and James Noble. Transient Typechecks Are (Almost) Free. In 33rd European Conference on Object-Oriented Programming (ECOOP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 134, pp. 5:1-5:28, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)


Copy BibTex To Clipboard

@InProceedings{roberts_et_al:LIPIcs.ECOOP.2019.5,
  author =	{Roberts, Richard and Marr, Stefan and Homer, Michael and Noble, James},
  title =	{{Transient Typechecks Are (Almost) Free}},
  booktitle =	{33rd European Conference on Object-Oriented Programming (ECOOP 2019)},
  pages =	{5:1--5:28},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-111-5},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{134},
  editor =	{Donaldson, Alastair F.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2019.5},
  URN =		{urn:nbn:de:0030-drops-107974},
  doi =		{10.4230/LIPIcs.ECOOP.2019.5},
  annote =	{Keywords: dynamic type checking, gradual types, optional types, Grace, Moth, object-oriented programming}
}
Document
Static Analysis for Asynchronous JavaScript Programs

Authors: Thodoris Sotiropoulos and Benjamin Livshits

Published in: LIPIcs, Volume 134, 33rd European Conference on Object-Oriented Programming (ECOOP 2019)


Abstract
Asynchrony has become an inherent element of JavaScript, as an effort to improve the scalability and performance of modern web applications. To this end, JavaScript provides programmers with a wide range of constructs and features for developing code that performs asynchronous computations, including but not limited to timers, promises, and non-blocking I/O. However, the data flow imposed by asynchrony is implicit, and not always well-understood by the developers who introduce many asynchrony-related bugs to their programs. Worse, there are few tools and techniques available for analyzing and reasoning about such asynchronous applications. In this work, we address this issue by designing and implementing one of the first static analysis schemes capable of dealing with almost all the asynchronous primitives of JavaScript up to the 7th edition of the ECMAScript specification. Specifically, we introduce the callback graph, a representation for capturing data flow between asynchronous code. We exploit the callback graph for designing a more precise analysis that respects the execution order between different asynchronous functions. We parameterize our analysis with one novel context-sensitivity flavor, and we end up with multiple analysis variations for building callback graph. We performed a number of experiments on a set of hand-written and real-world JavaScript programs. Our results show that our analysis can be applied to medium-sized programs achieving 79% precision, on average. The findings further suggest that analysis sensitivity is beneficial for the vast majority of the benchmarks. Specifically, it is able to improve precision by up to 28.5%, while it achieves an 88% precision on average without highly sacrificing performance.

Cite as

Thodoris Sotiropoulos and Benjamin Livshits. Static Analysis for Asynchronous JavaScript Programs. In 33rd European Conference on Object-Oriented Programming (ECOOP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 134, pp. 8:1-8:29, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)


Copy BibTex To Clipboard

@InProceedings{sotiropoulos_et_al:LIPIcs.ECOOP.2019.8,
  author =	{Sotiropoulos, Thodoris and Livshits, Benjamin},
  title =	{{Static Analysis for Asynchronous JavaScript Programs}},
  booktitle =	{33rd European Conference on Object-Oriented Programming (ECOOP 2019)},
  pages =	{8:1--8:29},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-111-5},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{134},
  editor =	{Donaldson, Alastair F.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2019.8},
  URN =		{urn:nbn:de:0030-drops-108007},
  doi =		{10.4230/LIPIcs.ECOOP.2019.8},
  annote =	{Keywords: static analysis, asynchrony, JavaScript}
}
Document
Reasoning About Foreign Function Interfaces Without Modelling the Foreign Language

Authors: Alexi Turcotte, Ellen Arteca, and Gregor Richards

Published in: LIPIcs, Volume 134, 33rd European Conference on Object-Oriented Programming (ECOOP 2019)


Abstract
Foreign function interfaces (FFIs) allow programs written in one language (called the host language) to call functions written in another language (called the guest language), and are widespread throughout modern programming languages, with C FFIs being the most prevalent. Unfortunately, reasoning about C FFIs can be very challenging, particularly when using traditional methods which necessitate a full model of the guest language in order to guarantee anything about the whole language. To address this, we propose a framework for defining whole language semantics of FFIs without needing to model the guest language, which makes reasoning about C FFIs feasible. We show that with such a semantics, one can guarantee some form of soundness of the overall language, as well as attribute errors in well-typed host language programs to the guest language. We also present an implementation of this scheme, Poseidon Lua, which shows a speedup over a traditional Lua C FFI.

Cite as

Alexi Turcotte, Ellen Arteca, and Gregor Richards. Reasoning About Foreign Function Interfaces Without Modelling the Foreign Language. In 33rd European Conference on Object-Oriented Programming (ECOOP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 134, pp. 16:1-16:32, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)


Copy BibTex To Clipboard

@InProceedings{turcotte_et_al:LIPIcs.ECOOP.2019.16,
  author =	{Turcotte, Alexi and Arteca, Ellen and Richards, Gregor},
  title =	{{Reasoning About Foreign Function Interfaces Without Modelling the Foreign Language}},
  booktitle =	{33rd European Conference on Object-Oriented Programming (ECOOP 2019)},
  pages =	{16:1--16:32},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-111-5},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{134},
  editor =	{Donaldson, Alastair F.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2019.16},
  URN =		{urn:nbn:de:0030-drops-108087},
  doi =		{10.4230/LIPIcs.ECOOP.2019.16},
  annote =	{Keywords: Formal Semantics, Language Interoperation, Lua, C, Foreign Function Interfaces}
}
Document
Concrete Types for TypeScript

Authors: Gregor Richards, Francesco Zappa Nardelli, and Jan Vitek

Published in: LIPIcs, Volume 37, 29th European Conference on Object-Oriented Programming (ECOOP 2015)


Abstract
Typescript extends JavaScript with optional type annotations that are, by design, unsound and, that the Typescript compiler discards as it emits code. This design point preserves programming idioms developers are familiar with, and allows them to leave their legacy code unchanged, while offering a measure of static error checking in parts of the program that have type annotations. We present an alternative design for TypeScript, one where it is possible to support the same degree of dynamism, but where types can be strengthened to provide hard guarantees. We report on an implementation, called StrongScript, that improves runtime performance of typed programs when run on a modified version of the V8 JavaScript engine.

Cite as

Gregor Richards, Francesco Zappa Nardelli, and Jan Vitek. Concrete Types for TypeScript. In 29th European Conference on Object-Oriented Programming (ECOOP 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 37, pp. 76-100, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)


Copy BibTex To Clipboard

@InProceedings{richards_et_al:LIPIcs.ECOOP.2015.76,
  author =	{Richards, Gregor and Zappa Nardelli, Francesco and Vitek, Jan},
  title =	{{Concrete Types for TypeScript}},
  booktitle =	{29th European Conference on Object-Oriented Programming (ECOOP 2015)},
  pages =	{76--100},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-86-6},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{37},
  editor =	{Boyland, John Tang},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2015.76},
  URN =		{urn:nbn:de:0030-drops-52185},
  doi =		{10.4230/LIPIcs.ECOOP.2015.76},
  annote =	{Keywords: Gradual typing, dynamic languages}
}
Document
Simple and Effective Type Check Removal through Lazy Basic Block Versioning

Authors: Maxime Chevalier-Boisvert and Marc Feeley

Published in: LIPIcs, Volume 37, 29th European Conference on Object-Oriented Programming (ECOOP 2015)


Abstract
Dynamically typed programming languages such as JavaScript and Python defer type checking to run time. In order to maximize performance, dynamic language VM implementations must attempt to eliminate redundant dynamic type checks. However, type inference analyses are often costly and involve tradeoffs between compilation time and resulting precision. This has lead to the creation of increasingly complex multi-tiered VM architectures. This paper introduces lazy basic block versioning, a simple JIT compilation technique which effectively removes redundant type checks from critical code paths. This novel approach lazily generates type-specialized versions of basic blocks on-the-fly while propagating context-dependent type information. This does not require the use of costly program analyses, is not restricted by the precision limitations of traditional type analyses and avoids the implementation complexity of speculative optimization techniques. We have implemented intraprocedural lazy basic block versioning in a JavaScript JIT compiler. This approach is compared with a classical flow-based type analysis. Lazy basic block versioning performs as well or better on all benchmarks. On average, 71% of type tests are eliminated, yielding speedups of up to 50%. We also show that our implementation generates more efficient machine code than TraceMonkey, a tracing JIT compiler for JavaScript, on several benchmarks. The combination of implementation simplicity, low algorithmic complexity and good run time performance makes basic block versioning attractive for baseline JIT compilers.

Cite as

Maxime Chevalier-Boisvert and Marc Feeley. Simple and Effective Type Check Removal through Lazy Basic Block Versioning. In 29th European Conference on Object-Oriented Programming (ECOOP 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 37, pp. 101-123, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)


Copy BibTex To Clipboard

@InProceedings{chevalierboisvert_et_al:LIPIcs.ECOOP.2015.101,
  author =	{Chevalier-Boisvert, Maxime and Feeley, Marc},
  title =	{{Simple and Effective Type Check Removal through Lazy Basic Block Versioning}},
  booktitle =	{29th European Conference on Object-Oriented Programming (ECOOP 2015)},
  pages =	{101--123},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-86-6},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{37},
  editor =	{Boyland, John Tang},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2015.101},
  URN =		{urn:nbn:de:0030-drops-52196},
  doi =		{10.4230/LIPIcs.ECOOP.2015.101},
  annote =	{Keywords: Just-In-Time Compilation, Dynamic Optimization, Type Checking, Code Generation, JavaScript}
}
Document
Hybrid DOM-Sensitive Change Impact Analysis for JavaScript

Authors: Saba Alimadadi, Ali Mesbah, and Karthik Pattabiraman

Published in: LIPIcs, Volume 37, 29th European Conference on Object-Oriented Programming (ECOOP 2015)


Abstract
JavaScript has grown to be among the most popular programming languages. However, performing change impact analysis on JavaScript applications is challenging due to features such as the seamless interplay with the DOM, event-driven and dynamic function calls, and asynchronous client/server communication. We first perform an empirical study of change propagation, the results of which show that the DOM-related and dynamic features of JavaScript need to be taken into consideration in the analysis since they affect change impact propagation. We propose a DOM-sensitive hybrid change impact analysis technique for Javascript through a combination of static and dynamic analysis. The proposed approach incorporates a novel ranking algorithm for indicating the importance of each entity in the impact set. Our approach is implemented in a tool called Tochal. The results of our evaluation reveal that Tochal provides a more complete analysis compared to static or dynamic methods. Moreover, through an industrial controlled experiment, we find that Tochal helps developers by improving their task completion duration by 78% and accuracy by 223%.

Cite as

Saba Alimadadi, Ali Mesbah, and Karthik Pattabiraman. Hybrid DOM-Sensitive Change Impact Analysis for JavaScript. In 29th European Conference on Object-Oriented Programming (ECOOP 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 37, pp. 321-345, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)


Copy BibTex To Clipboard

@InProceedings{alimadadi_et_al:LIPIcs.ECOOP.2015.321,
  author =	{Alimadadi, Saba and Mesbah, Ali and Pattabiraman, Karthik},
  title =	{{Hybrid DOM-Sensitive Change Impact Analysis for JavaScript}},
  booktitle =	{29th European Conference on Object-Oriented Programming (ECOOP 2015)},
  pages =	{321--345},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-86-6},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{37},
  editor =	{Boyland, John Tang},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2015.321},
  URN =		{urn:nbn:de:0030-drops-52280},
  doi =		{10.4230/LIPIcs.ECOOP.2015.321},
  annote =	{Keywords: Change impact analysis, JavaScript, hybrid analysis}
}
Document
The Good, the Bad, and the Ugly: An Empirical Study of Implicit Type Conversions in JavaScript

Authors: Michael Pradel and Koushik Sen

Published in: LIPIcs, Volume 37, 29th European Conference on Object-Oriented Programming (ECOOP 2015)


Abstract
Most popular programming languages support situations where a value of one type is converted into a value of another type without any explicit cast. Such implicit type conversions, or type coercions, are a highly controversial language feature. Proponents argue that type coercions enable writing concise code. Opponents argue that type coercions are error-prone and that they reduce the understandability of programs. This paper studies the use of type coercions in JavaScript, a language notorious for its widespread use of coercions. We dynamically analyze hundreds of programs, including real-world web applications and popular benchmark programs. We find that coercions are widely used (in 80.42% of all function executions) and that most coercions are likely to be harmless (98.85%). Furthermore, we identify a set of rarely occurring and potentially harmful coercions that safer subsets of JavaScript or future language designs may want to disallow. Our results suggest that type coercions are significantly less evil than commonly assumed and that analyses targeted at real-world JavaScript programs must consider coercions.

Cite as

Michael Pradel and Koushik Sen. The Good, the Bad, and the Ugly: An Empirical Study of Implicit Type Conversions in JavaScript. In 29th European Conference on Object-Oriented Programming (ECOOP 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 37, pp. 519-541, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)


Copy BibTex To Clipboard

@InProceedings{pradel_et_al:LIPIcs.ECOOP.2015.519,
  author =	{Pradel, Michael and Sen, Koushik},
  title =	{{The Good, the Bad, and the Ugly: An Empirical Study of Implicit Type Conversions in JavaScript}},
  booktitle =	{29th European Conference on Object-Oriented Programming (ECOOP 2015)},
  pages =	{519--541},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-86-6},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{37},
  editor =	{Boyland, John Tang},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2015.519},
  URN =		{urn:nbn:de:0030-drops-52367},
  doi =		{10.4230/LIPIcs.ECOOP.2015.519},
  annote =	{Keywords: Types, Type coercions, JavaScript, Dynamically typed languages}
}
Document
Refined Criteria for Gradual Typing

Authors: Jeremy G. Siek, Michael M. Vitousek, Matteo Cimini, and John Tang Boyland

Published in: LIPIcs, Volume 32, 1st Summit on Advances in Programming Languages (SNAPL 2015)


Abstract
Siek and Taha [2006] coined the term gradual typing to describe a theory for integrating static and dynamic typing within a single language that 1) puts the programmer in control of which regions of code are statically or dynamically typed and 2) enables the gradual evolution of code between the two typing disciplines. Since 2006, the term gradual typing has become quite popular but its meaning has become diluted to encompass anything related to the integration of static and dynamic typing. This dilution is partly the fault of the original paper, which provided an incomplete formal characterization of what it means to be gradually typed. In this paper we draw a crisp line in the sand that includes a new formal property, named the gradual guarantee, that relates the behavior of programs that differ only with respect to their type annotations. We argue that the gradual guarantee provides important guidance for designers of gradually typed languages. We survey the gradual typing literature, critiquing designs in light of the gradual guarantee. We also report on a mechanized proof that the gradual guarantee holds for the Gradually Typed Lambda Calculus.

Cite as

Jeremy G. Siek, Michael M. Vitousek, Matteo Cimini, and John Tang Boyland. Refined Criteria for Gradual Typing. In 1st Summit on Advances in Programming Languages (SNAPL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 32, pp. 274-293, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)


Copy BibTex To Clipboard

@InProceedings{siek_et_al:LIPIcs.SNAPL.2015.274,
  author =	{Siek, Jeremy G. and Vitousek, Michael M. and Cimini, Matteo and Boyland, John Tang},
  title =	{{Refined Criteria for Gradual Typing}},
  booktitle =	{1st Summit on Advances in Programming Languages (SNAPL 2015)},
  pages =	{274--293},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-80-4},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{32},
  editor =	{Ball, Thomas and Bodík, Rastislav and Krishnamurthi, Shriram and Lerner, Benjamin S. and Morriset, Greg},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SNAPL.2015.274},
  URN =		{urn:nbn:de:0030-drops-50312},
  doi =		{10.4230/LIPIcs.SNAPL.2015.274},
  annote =	{Keywords: gradual typing, type systems, semantics, dynamic languages}
}
  • Refine by Author
  • 5 Richards, Gregor
  • 2 Arteca, Ellen
  • 2 Lhoták, Ondřej
  • 2 Nieto, Abel
  • 2 Rapoport, Marianna
  • Show More...

  • Refine by Classification
  • 4 Software and its engineering → Interoperability
  • 3 Software and its engineering → General programming languages
  • 3 Software and its engineering → Semantics
  • 2 Software and its engineering → Interpreters
  • 2 Theory of computation → Operational semantics
  • Show More...

  • Refine by Keyword
  • 4 JavaScript
  • 4 gradual typing
  • 3 type systems
  • 2 blame calculus
  • 2 dynamic languages
  • Show More...

  • Refine by Type
  • 14 document

  • Refine by Publication Year
  • 7 2019
  • 5 2015
  • 2 2020

Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail