4 Search Results for "Palsberg, Jens"

Document
Artifact
DOI: 10.4230/DARTS.8.2.3
Compiling Volatile Correctly in Java (Artifact)

Authors: Shuyang Liu, John Bender, and Jens Palsberg

Published in: DARTS, Volume 8, Issue 2, Special Issue of the 36th European Conference on Object-Oriented Programming (ECOOP 2022)

Abstract
The compilation scheme for Volatile accesses in the OpenJDK 9 HotSpot Java Virtual Machine has a major problem that persists despite a recent bug report and a long discussion. One of the suggested fixes is to let Java compile Volatile accesses in the same way as C/C++11. However, we show that this approach is invalid for Java. Indeed, we show a set of optimizations that is valid for C/C++11 but invalid for Java, while the compilation scheme is similar. We prove the correctness of the compilation scheme to Power and x86 and a suite of valid optimizations in Java. Our proofs are based on a language model that we validate by proving key properties such as the DRF-SC theorem and by running litmus tests via our implementation of Java in Herd7.
Cite as

Shuyang Liu, John Bender, and Jens Palsberg. Compiling Volatile Correctly in Java (Artifact). In Special Issue of the 36th European Conference on Object-Oriented Programming (ECOOP 2022). Dagstuhl Artifacts Series (DARTS), Volume 8, Issue 2, pp. 3:1-3:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@Article{liu_et_al:DARTS.8.2.3,
  author =	{Liu, Shuyang and Bender, John and Palsberg, Jens},
  title =	{{Compiling Volatile Correctly in Java (Artifact)}},
  pages =	{3:1--3:2},
  journal =	{Dagstuhl Artifacts Series},
  ISSN =	{2509-8195},
  year =	{2022},
  volume =	{8},
  number =	{2},
  editor =	{Liu, Shuyang and Bender, John and Palsberg, Jens},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DARTS.8.2.3},
  URN =		{urn:nbn:de:0030-drops-162018},
  doi =		{10.4230/DARTS.8.2.3},
  annote =	{Keywords: formal semantics, concurrency, compilation}
}
Document
DOI: 10.4230/LIPIcs.ECOOP.2022.6
Compiling Volatile Correctly in Java

Authors: Shuyang Liu, John Bender, and Jens Palsberg

Published in: LIPIcs, Volume 222, 36th European Conference on Object-Oriented Programming (ECOOP 2022)

Abstract
The compilation scheme for Volatile accesses in the OpenJDK 9 HotSpot Java Virtual Machine has a major problem that persists despite a recent bug report and a long discussion. One of the suggested fixes is to let Java compile Volatile accesses in the same way as C/C++11. However, we show that this approach is invalid for Java. Indeed, we show a set of optimizations that is valid for C/C++11 but invalid for Java, while the compilation scheme is similar. We prove the correctness of the compilation scheme to Power and x86 and a suite of valid optimizations in Java. Our proofs are based on a language model that we validate by proving key properties such as the DRF-SC theorem and by running litmus tests via our implementation of Java in Herd7.
Cite as

Shuyang Liu, John Bender, and Jens Palsberg. Compiling Volatile Correctly in Java. In 36th European Conference on Object-Oriented Programming (ECOOP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 222, pp. 6:1-6:26, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{liu_et_al:LIPIcs.ECOOP.2022.6,
  author =	{Liu, Shuyang and Bender, John and Palsberg, Jens},
  title =	{{Compiling Volatile Correctly in Java}},
  booktitle =	{36th European Conference on Object-Oriented Programming (ECOOP 2022)},
  pages =	{6:1--6:26},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-225-9},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{222},
  editor =	{Ali, Karim and Vitek, Jan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2022.6},
  URN =		{urn:nbn:de:0030-drops-162346},
  doi =		{10.4230/LIPIcs.ECOOP.2022.6},
  annote =	{Keywords: formal semantics, concurrency, compilation}
}
Document
DOI: 10.4230/LIPIcs.ECOOP.2015.371
Type Inference for Place-Oblivious Objects

Authors: Riyaz Haque and Jens Palsberg

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

Abstract
In a distributed system, access to local data is much faster than access to remote data. As a help to programmers, some languages require every access to be local. A program in those languages can access remote data via first a shift of the place of computation and then a local access. To enforce this discipline, researchers have presented type systems that determine whether every access is local and every place shift is appropriate. However, those type systems fall short of handling a common programming pattern that we call place-oblivious objects. Such objects safely access other objects without knowledge of their place. In response, we present the first type system for place-oblivious objects along with an efficient inference algorithm and a proof that inference is P-complete. Our example language extends the Abadi-Cardelli object calculus with place shift and existential types, and our implementation has inferred types for some microbenchmarks.
Cite as

Riyaz Haque and Jens Palsberg. Type Inference for Place-Oblivious Objects. In 29th European Conference on Object-Oriented Programming (ECOOP 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 37, pp. 371-395, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{haque_et_al:LIPIcs.ECOOP.2015.371,
  author =	{Haque, Riyaz and Palsberg, Jens},
  title =	{{Type Inference for Place-Oblivious Objects}},
  booktitle =	{29th European Conference on Object-Oriented Programming (ECOOP 2015)},
  pages =	{371--395},
  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-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2015.371},
  URN =		{urn:nbn:de:0030-drops-52223},
  doi =		{10.4230/LIPIcs.ECOOP.2015.371},
  annote =	{Keywords: parallelism, locality, types}
}
Document
DOI: 10.4230/DagSemRep.216
The Semantic Challenge of Object-Oriented Programming (Dagstuhl Seminar 98261)

Authors: Luca Cardelli, Achim Jung, Peter O'Hearn, and Jens Palsberg

Published in: Dagstuhl Seminar Reports. Dagstuhl Seminar Reports, Volume 1 (2021)

Abstract
Cite as

Luca Cardelli, Achim Jung, Peter O'Hearn, and Jens Palsberg. The Semantic Challenge of Object-Oriented Programming (Dagstuhl Seminar 98261). Dagstuhl Seminar Report 216, pp. 1-14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (1999)

Copy BibTex To Clipboard

@TechReport{cardelli_et_al:DagSemRep.216,
  author =	{Cardelli, Luca and Jung, Achim and O'Hearn, Peter and Palsberg, Jens},
  title =	{{The Semantic Challenge of Object-Oriented Programming (Dagstuhl Seminar 98261)}},
  pages =	{1--14},
  ISSN =	{1619-0203},
  year =	{1999},
  type = 	{Dagstuhl Seminar Report},
  number =	{216},
  institution =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DagSemRep.216},
  URN =		{urn:nbn:de:0030-drops-151022},
  doi =		{10.4230/DagSemRep.216},
}
  • Refine by Author
  • 4 Palsberg, Jens
  • 2 Bender, John
  • 2 Liu, Shuyang
  • 1 Cardelli, Luca
  • 1 Haque, Riyaz
  • Show More...

  • Refine by Classification
  • 2 Software and its engineering → Semantics

  • Refine by Keyword
  • 2 compilation
  • 2 concurrency
  • 2 formal semantics
  • 1 locality
  • 1 parallelism
  • Show More...

  • Refine by Type
  • 4 document

  • Refine by Publication Year
  • 2 2022
  • 1 1999
  • 1 2015

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
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact