---
_id: '13179'
abstract:
- lang: eng
text: "Writing concurrent code that is both correct and efficient is notoriously
difficult. Thus, programmers often prefer to use synchronization abstractions,
which render code simpler and easier to reason about. Despite a wealth of work
on this topic, there is still a gap between the rich semantics provided by synchronization
abstractions in modern programming languages—specifically, fair FIFO ordering
of synchronization requests and support for abortable operations—and frameworks
for implementing it correctly and efficiently. Supporting such semantics is critical
given the rising popularity of constructs for asynchronous programming, such as
coroutines, which abort frequently and are cheaper to suspend and resume compared
to native threads.\r\n\r\nThis paper introduces a new framework called CancellableQueueSynchronizer
(CQS), which enables simple yet efficient implementations of a wide range of fair
and abortable synchronization primitives: mutexes, semaphores, barriers, count-down
latches, and blocking pools. Our main contribution is algorithmic, as implementing
both fairness and abortability efficiently at this level of generality is non-trivial.
Importantly, all our algorithms, including the CQS framework and the primitives
built on top of it, come with formal proofs in the Iris framework for Coq for
many of their properties. These proofs are modular, so it is easy to show correctness
for new primitives implemented on top of CQS. From a practical perspective, implementation
of CQS for native threads on the JVM improves throughput by up to two orders of
magnitude over Java’s AbstractQueuedSynchronizer, the only practical abstraction
offering similar semantics. Further, we successfully integrated CQS as a core
component of the popular Kotlin Coroutines library, validating the framework’s
practical impact and expressiveness in a real-world environment. In sum, CancellableQueueSynchronizer
is the first framework to combine expressiveness with formal guarantees and solid
practical performance. Our approach should be extensible to other languages and
families of synchronization primitives."
article_number: '116'
article_processing_charge: No
article_type: original
author:
- first_name: Nikita
full_name: Koval, Nikita
id: 2F4DB10C-F248-11E8-B48F-1D18A9856A87
last_name: Koval
- first_name: Dmitry
full_name: Khalanskiy, Dmitry
last_name: Khalanskiy
- first_name: Dan-Adrian
full_name: Alistarh, Dan-Adrian
id: 4A899BFC-F248-11E8-B48F-1D18A9856A87
last_name: Alistarh
orcid: 0000-0003-3650-940X
citation:
ama: 'Koval N, Khalanskiy D, Alistarh D-A. CQS: A formally-verified framework for
fair and abortable synchronization. Proceedings of the ACM on Programming Languages.
2023;7. doi:10.1145/3591230'
apa: 'Koval, N., Khalanskiy, D., & Alistarh, D.-A. (2023). CQS: A formally-verified
framework for fair and abortable synchronization. Proceedings of the ACM on
Programming Languages. Association for Computing Machinery . https://doi.org/10.1145/3591230'
chicago: 'Koval, Nikita, Dmitry Khalanskiy, and Dan-Adrian Alistarh. “CQS: A Formally-Verified
Framework for Fair and Abortable Synchronization.” Proceedings of the ACM on
Programming Languages. Association for Computing Machinery , 2023. https://doi.org/10.1145/3591230.'
ieee: 'N. Koval, D. Khalanskiy, and D.-A. Alistarh, “CQS: A formally-verified framework
for fair and abortable synchronization,” Proceedings of the ACM on Programming
Languages, vol. 7. Association for Computing Machinery , 2023.'
ista: 'Koval N, Khalanskiy D, Alistarh D-A. 2023. CQS: A formally-verified framework
for fair and abortable synchronization. Proceedings of the ACM on Programming
Languages. 7, 116.'
mla: 'Koval, Nikita, et al. “CQS: A Formally-Verified Framework for Fair and Abortable
Synchronization.” Proceedings of the ACM on Programming Languages, vol.
7, 116, Association for Computing Machinery , 2023, doi:10.1145/3591230.'
short: N. Koval, D. Khalanskiy, D.-A. Alistarh, Proceedings of the ACM on Programming
Languages 7 (2023).
date_created: 2023-07-02T22:00:43Z
date_published: 2023-06-06T00:00:00Z
date_updated: 2023-07-17T08:43:19Z
day: '06'
ddc:
- '000'
department:
- _id: DaAl
doi: 10.1145/3591230
file:
- access_level: open_access
checksum: 5dba6e73f0ed79adbdae14d165bc2f68
content_type: application/pdf
creator: alisjak
date_created: 2023-07-03T13:09:39Z
date_updated: 2023-07-03T13:09:39Z
file_id: '13187'
file_name: 2023_ACMProgram.Lang._Koval.pdf
file_size: 1266773
relation: main_file
success: 1
file_date_updated: 2023-07-03T13:09:39Z
has_accepted_license: '1'
intvolume: ' 7'
language:
- iso: eng
month: '06'
oa: 1
oa_version: Published Version
publication: Proceedings of the ACM on Programming Languages
publication_identifier:
eissn:
- 2475-1421
publication_status: published
publisher: 'Association for Computing Machinery '
quality_controlled: '1'
scopus_import: '1'
status: public
title: 'CQS: A formally-verified framework for fair and abortable synchronization'
tmp:
image: /images/cc_by.png
legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
short: CC BY (4.0)
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 7
year: '2023'
...
---
_id: '10153'
abstract:
- lang: eng
text: "Gradual typing is a principled means for mixing typed and untyped code. But
typed and untyped code often exhibit different programming patterns. There is
already substantial research investigating gradually giving types to code exhibiting
typical untyped patterns, and some research investigating gradually removing types
from code exhibiting typical typed patterns. This paper investigates how to extend
these established gradual-typing concepts to give formal guarantees not only about
how to change types as code evolves but also about how to change such programming
patterns as well.\r\n\r\nIn particular, we explore mixing untyped \"structural\"
code with typed \"nominal\" code in an object-oriented language. But whereas previous
work only allowed \"nominal\" objects to be treated as \"structural\" objects,
we also allow \"structural\" objects to dynamically acquire certain nominal types,
namely interfaces. We present a calculus that supports such \"cross-paradigm\"
code migration and interoperation in a manner satisfying both the static and dynamic
gradual guarantees, and demonstrate that the calculus can be implemented efficiently."
acknowledgement: "We thank the reviewers for their valuable suggestions towards improving
the paper. We also \r\nthank Mae Milano and Adrian Sampson, as well as the members
of the Programming Languages Discussion Group at Cornell University and of the Programming
Research Laboratory at Northeastern University, for their helpful feedback on preliminary
findings of this work.\r\n\r\nThis material is based upon work supported in part
by the National Science Foundation (NSF) through grant CCF-1350182 and the Austrian
Science Fund (FWF) through grant Z211-N23 (Wittgenstein~Award).\r\nAny opinions,
findings, and conclusions or recommendations expressed in this material are those
of the authors and do not necessarily reflect the views of the NSF or the FWF."
article_number: '127'
article_processing_charge: No
article_type: original
author:
- first_name: Fabian
full_name: Mühlböck, Fabian
id: 6395C5F6-89DF-11E9-9C97-6BDFE5697425
last_name: Mühlböck
orcid: 0000-0003-1548-0177
- first_name: Ross
full_name: Tate, Ross
last_name: Tate
citation:
ama: Mühlböck F, Tate R. Transitioning from structural to nominal code with efficient
gradual typing. Proceedings of the ACM on Programming Languages. 2021;5.
doi:10.1145/3485504
apa: 'Mühlböck, F., & Tate, R. (2021). Transitioning from structural to nominal
code with efficient gradual typing. Proceedings of the ACM on Programming Languages.
Chicago, IL, United States: Association for Computing Machinery. https://doi.org/10.1145/3485504'
chicago: Mühlböck, Fabian, and Ross Tate. “Transitioning from Structural to Nominal
Code with Efficient Gradual Typing.” Proceedings of the ACM on Programming
Languages. Association for Computing Machinery, 2021. https://doi.org/10.1145/3485504.
ieee: F. Mühlböck and R. Tate, “Transitioning from structural to nominal code with
efficient gradual typing,” Proceedings of the ACM on Programming Languages,
vol. 5. Association for Computing Machinery, 2021.
ista: Mühlböck F, Tate R. 2021. Transitioning from structural to nominal code with
efficient gradual typing. Proceedings of the ACM on Programming Languages. 5,
127.
mla: Mühlböck, Fabian, and Ross Tate. “Transitioning from Structural to Nominal
Code with Efficient Gradual Typing.” Proceedings of the ACM on Programming
Languages, vol. 5, 127, Association for Computing Machinery, 2021, doi:10.1145/3485504.
short: F. Mühlböck, R. Tate, Proceedings of the ACM on Programming Languages 5 (2021).
conference:
end_date: 2021-10-23
location: Chicago, IL, United States
name: 'OOPSLA: Object-Oriented Programming, Systems, Languages, and Applications'
start_date: 2021-10-17
date_created: 2021-10-19T12:48:44Z
date_published: 2021-10-15T00:00:00Z
date_updated: 2021-11-12T11:30:07Z
day: '15'
ddc:
- '005'
department:
- _id: ToHe
doi: 10.1145/3485504
file:
- access_level: open_access
checksum: 71011efd2da771cafdec7f0d9693f8c1
content_type: application/pdf
creator: fmuehlbo
date_created: 2021-10-19T12:52:23Z
date_updated: 2021-10-19T12:52:23Z
file_id: '10154'
file_name: monnom-oopsla21.pdf
file_size: 770269
relation: main_file
success: 1
file_date_updated: 2021-10-19T12:52:23Z
has_accepted_license: '1'
intvolume: ' 5'
keyword:
- gradual typing
- gradual guarantee
- nominal
- structural
- call tags
language:
- iso: eng
license: https://creativecommons.org/licenses/by-nd/4.0/
month: '10'
oa: 1
oa_version: Published Version
project:
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: Z211
name: The Wittgenstein Prize
publication: Proceedings of the ACM on Programming Languages
publication_identifier:
eissn:
- 2475-1421
publication_status: published
publisher: Association for Computing Machinery
quality_controlled: '1'
status: public
title: Transitioning from structural to nominal code with efficient gradual typing
tmp:
image: /image/cc_by_nd.png
legal_code_url: https://creativecommons.org/licenses/by-nd/4.0/legalcode
name: Creative Commons Attribution-NoDerivatives 4.0 International (CC BY-ND 4.0)
short: CC BY-ND (4.0)
type: journal_article
user_id: 8b945eb4-e2f2-11eb-945a-df72226e66a9
volume: 5
year: '2021'
...
---
_id: '10191'
abstract:
- lang: eng
text: "In this work we solve the algorithmic problem of consistency verification
for the TSO and PSO memory models given a reads-from map, denoted VTSO-rf and
VPSO-rf, respectively. For an execution of n events over k threads and d variables,
we establish novel bounds that scale as nk+1 for TSO and as nk+1· min(nk2, 2k·
d) for PSO. Moreover, based on our solution to these problems, we develop an SMC
algorithm under TSO and PSO that uses the RF equivalence. The algorithm is exploration-optimal,
in the sense that it is guaranteed to explore each class of the RF partitioning
exactly once, and spends polynomial time per class when k is bounded. Finally,
we implement all our algorithms in the SMC tool Nidhugg, and perform a large number
of experiments over benchmarks from existing literature. Our experimental results
show that our algorithms for VTSO-rf and VPSO-rf provide significant scalability
improvements over standard alternatives. Moreover, when used for SMC, the RF partitioning
is often much coarser than the standard Shasha-Snir partitioning for TSO/PSO,
which yields a significant speedup in the model checking task.\r\n\r\n"
acknowledgement: "The research was partially funded by the ERC CoG 863818 (ForM-SMArt)
and the Vienna Science\r\nand Technology Fund (WWTF) through project ICT15-003."
article_number: '164'
article_processing_charge: No
article_type: original
arxiv: 1
author:
- first_name: Truc Lam
full_name: Bui, Truc Lam
last_name: Bui
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Tushar
full_name: Gautam, Tushar
last_name: Gautam
- first_name: Andreas
full_name: Pavlogiannis, Andreas
id: 49704004-F248-11E8-B48F-1D18A9856A87
last_name: Pavlogiannis
orcid: 0000-0002-8943-0722
- first_name: Viktor
full_name: Toman, Viktor
id: 3AF3DA7C-F248-11E8-B48F-1D18A9856A87
last_name: Toman
orcid: 0000-0001-9036-063X
citation:
ama: Bui TL, Chatterjee K, Gautam T, Pavlogiannis A, Toman V. The reads-from equivalence
for the TSO and PSO memory models. Proceedings of the ACM on Programming Languages.
2021;5(OOPSLA). doi:10.1145/3485541
apa: Bui, T. L., Chatterjee, K., Gautam, T., Pavlogiannis, A., & Toman, V. (2021).
The reads-from equivalence for the TSO and PSO memory models. Proceedings of
the ACM on Programming Languages. Association for Computing Machinery. https://doi.org/10.1145/3485541
chicago: Bui, Truc Lam, Krishnendu Chatterjee, Tushar Gautam, Andreas Pavlogiannis,
and Viktor Toman. “The Reads-from Equivalence for the TSO and PSO Memory Models.”
Proceedings of the ACM on Programming Languages. Association for Computing
Machinery, 2021. https://doi.org/10.1145/3485541.
ieee: T. L. Bui, K. Chatterjee, T. Gautam, A. Pavlogiannis, and V. Toman, “The reads-from
equivalence for the TSO and PSO memory models,” Proceedings of the ACM on Programming
Languages, vol. 5, no. OOPSLA. Association for Computing Machinery, 2021.
ista: Bui TL, Chatterjee K, Gautam T, Pavlogiannis A, Toman V. 2021. The reads-from
equivalence for the TSO and PSO memory models. Proceedings of the ACM on Programming
Languages. 5(OOPSLA), 164.
mla: Bui, Truc Lam, et al. “The Reads-from Equivalence for the TSO and PSO Memory
Models.” Proceedings of the ACM on Programming Languages, vol. 5, no. OOPSLA,
164, Association for Computing Machinery, 2021, doi:10.1145/3485541.
short: T.L. Bui, K. Chatterjee, T. Gautam, A. Pavlogiannis, V. Toman, Proceedings
of the ACM on Programming Languages 5 (2021).
date_created: 2021-10-27T15:05:34Z
date_published: 2021-10-15T00:00:00Z
date_updated: 2025-07-14T09:10:16Z
day: '15'
ddc:
- '000'
department:
- _id: GradSch
- _id: KrCh
doi: 10.1145/3485541
ec_funded: 1
external_id:
arxiv:
- '2011.11763'
file:
- access_level: open_access
checksum: 9d6dce7b611853c529bb7b1915ac579e
content_type: application/pdf
creator: cchlebak
date_created: 2021-11-04T07:24:48Z
date_updated: 2021-11-04T07:24:48Z
file_id: '10215'
file_name: 2021_ProcACMPL_Bui.pdf
file_size: 2903485
relation: main_file
success: 1
file_date_updated: 2021-11-04T07:24:48Z
has_accepted_license: '1'
intvolume: ' 5'
issue: OOPSLA
keyword:
- safety
- risk
- reliability and quality
- software
language:
- iso: eng
month: '10'
oa: 1
oa_version: Published Version
project:
- _id: 0599E47C-7A3F-11EA-A408-12923DDC885E
call_identifier: H2020
grant_number: '863818'
name: 'Formal Methods for Stochastic Models: Algorithms and Applications'
- _id: 25892FC0-B435-11E9-9278-68D0E5697425
grant_number: ICT15-003
name: Efficient Algorithms for Computer Aided Verification
publication: Proceedings of the ACM on Programming Languages
publication_identifier:
eissn:
- 2475-1421
publication_status: published
publisher: Association for Computing Machinery
quality_controlled: '1'
related_material:
record:
- id: '10199'
relation: dissertation_contains
status: public
scopus_import: '1'
status: public
title: The reads-from equivalence for the TSO and PSO memory models
tmp:
image: /images/cc_by.png
legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
short: CC BY (4.0)
type: journal_article
user_id: 8b945eb4-e2f2-11eb-945a-df72226e66a9
volume: 5
year: '2021'
...
---
_id: '8324'
abstract:
- lang: eng
text: The notion of program sensitivity (aka Lipschitz continuity) specifies that
changes in the program input result in proportional changes to the program output.
For probabilistic programs the notion is naturally extended to expected sensitivity.
A previous approach develops a relational program logic framework for proving
expected sensitivity of probabilistic while loops, where the number of iterations
is fixed and bounded. In this work, we consider probabilistic while loops where
the number of iterations is not fixed, but randomized and depends on the initial
input values. We present a sound approach for proving expected sensitivity of
such programs. Our sound approach is martingale-based and can be automated through
existing martingale-synthesis algorithms. Furthermore, our approach is compositional
for sequential composition of while loops under a mild side condition. We demonstrate
the effectiveness of our approach on several classical examples from Gambler's
Ruin, stochastic hybrid systems and stochastic gradient descent. We also present
experimental results showing that our automated approach can handle various probabilistic
programs in the literature.
acknowledgement: We thank anonymous reviewers for helpful comments, especially for
pointing to us a scenario of piecewise-linear approximation (Remark5). The research
was partially supported by the National Natural Science Foundation of China (NSFC)
under Grant No. 61802254, 61672229, 61832015,61772336,11871221 and Austrian Science
Fund (FWF) NFN under Grant No. S11407-N23 (RiSE/SHiNE). We thank Prof. Yuxi Fu,
director of the BASICS Lab at Shanghai Jiao Tong University, for his support.
article_number: '25'
article_processing_charge: No
arxiv: 1
author:
- first_name: Peixin
full_name: Wang, Peixin
last_name: Wang
- first_name: Hongfei
full_name: Fu, Hongfei
last_name: Fu
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Yuxin
full_name: Deng, Yuxin
last_name: Deng
- first_name: Ming
full_name: Xu, Ming
last_name: Xu
citation:
ama: 'Wang P, Fu H, Chatterjee K, Deng Y, Xu M. Proving expected sensitivity of
probabilistic programs with randomized variable-dependent termination time. In:
Proceedings of the ACM on Programming Languages. Vol 4. ACM; 2020. doi:10.1145/3371093'
apa: Wang, P., Fu, H., Chatterjee, K., Deng, Y., & Xu, M. (2020). Proving expected
sensitivity of probabilistic programs with randomized variable-dependent termination
time. In Proceedings of the ACM on Programming Languages (Vol. 4). ACM.
https://doi.org/10.1145/3371093
chicago: Wang, Peixin, Hongfei Fu, Krishnendu Chatterjee, Yuxin Deng, and Ming Xu.
“Proving Expected Sensitivity of Probabilistic Programs with Randomized Variable-Dependent
Termination Time.” In Proceedings of the ACM on Programming Languages,
Vol. 4. ACM, 2020. https://doi.org/10.1145/3371093.
ieee: P. Wang, H. Fu, K. Chatterjee, Y. Deng, and M. Xu, “Proving expected sensitivity
of probabilistic programs with randomized variable-dependent termination time,”
in Proceedings of the ACM on Programming Languages, 2020, vol. 4, no. POPL.
ista: Wang P, Fu H, Chatterjee K, Deng Y, Xu M. 2020. Proving expected sensitivity
of probabilistic programs with randomized variable-dependent termination time.
Proceedings of the ACM on Programming Languages. vol. 4, 25.
mla: Wang, Peixin, et al. “Proving Expected Sensitivity of Probabilistic Programs
with Randomized Variable-Dependent Termination Time.” Proceedings of the ACM
on Programming Languages, vol. 4, no. POPL, 25, ACM, 2020, doi:10.1145/3371093.
short: P. Wang, H. Fu, K. Chatterjee, Y. Deng, M. Xu, in:, Proceedings of the ACM
on Programming Languages, ACM, 2020.
date_created: 2020-08-30T22:01:12Z
date_published: 2020-01-01T00:00:00Z
date_updated: 2024-02-22T15:16:45Z
day: '01'
ddc:
- '004'
department:
- _id: KrCh
doi: 10.1145/3371093
external_id:
arxiv:
- '1902.04744'
file:
- access_level: open_access
checksum: c6193d109ff4ecb17e7a6513d8eb34c0
content_type: application/pdf
creator: cziletti
date_created: 2020-09-01T11:12:58Z
date_updated: 2020-09-01T11:12:58Z
file_id: '8328'
file_name: 2019_ACM_POPL_Wang.pdf
file_size: 564151
relation: main_file
success: 1
file_date_updated: 2020-09-01T11:12:58Z
has_accepted_license: '1'
intvolume: ' 4'
issue: POPL
language:
- iso: eng
month: '01'
oa: 1
oa_version: Published Version
project:
- _id: 25863FF4-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S11407
name: Game Theory
publication: Proceedings of the ACM on Programming Languages
publication_identifier:
eissn:
- 2475-1421
publication_status: published
publisher: ACM
quality_controlled: '1'
related_material:
link:
- relation: software
url: https://doi.org/10.5281/zenodo.3533633
scopus_import: '1'
status: public
title: Proving expected sensitivity of probabilistic programs with randomized variable-dependent
termination time
tmp:
image: /images/cc_by.png
legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
short: CC BY (4.0)
type: conference
user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87
volume: 4
year: '2020'
...
---
_id: '10190'
abstract:
- lang: eng
text: 'The verification of concurrent programs remains an open challenge, as thread
interaction has to be accounted for, which leads to state-space explosion. Stateless
model checking battles this problem by exploring traces rather than states of
the program. As there are exponentially many traces, dynamic partial-order reduction
(DPOR) techniques are used to partition the trace space into equivalence classes,
and explore a few representatives from each class. The standard equivalence that
underlies most DPOR techniques is the happens-before equivalence, however recent
works have spawned a vivid interest towards coarser equivalences. The efficiency
of such approaches is a product of two parameters: (i) the size of the partitioning
induced by the equivalence, and (ii) the time spent by the exploration algorithm
in each class of the partitioning. In this work, we present a new equivalence,
called value-happens-before and show that it has two appealing features. First,
value-happens-before is always at least as coarse as the happens-before equivalence,
and can be even exponentially coarser. Second, the value-happens-before partitioning
is efficiently explorable when the number of threads is bounded. We present an
algorithm called value-centric DPOR (VCDPOR), which explores the underlying partitioning
using polynomial time per class. Finally, we perform an experimental evaluation
of VCDPOR on various benchmarks, and compare it against other state-of-the-art
approaches. Our results show that value-happens-before typically induces a significant
reduction in the size of the underlying partitioning, which leads to a considerable
reduction in the running time for exploring the whole partitioning.'
acknowledgement: "The authors would also like to thank anonymous referees for their
valuable comments and helpful suggestions. This work is supported by the Austrian
Science Fund (FWF) NFN grants S11407-N23 (RiSE/SHiNE) and S11402-N23 (RiSE/SHiNE),
by the Vienna Science and Technology Fund (WWTF) Project ICT15-003, and by the Austrian
Science Fund (FWF) Schrodinger grant J-4220.\r\n"
article_number: '124'
article_processing_charge: No
arxiv: 1
author:
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Andreas
full_name: Pavlogiannis, Andreas
id: 49704004-F248-11E8-B48F-1D18A9856A87
last_name: Pavlogiannis
orcid: 0000-0002-8943-0722
- first_name: Viktor
full_name: Toman, Viktor
id: 3AF3DA7C-F248-11E8-B48F-1D18A9856A87
last_name: Toman
orcid: 0000-0001-9036-063X
citation:
ama: 'Chatterjee K, Pavlogiannis A, Toman V. Value-centric dynamic partial order
reduction. In: Proceedings of the 34th ACM International Conference on Object-Oriented
Programming, Systems, Languages, and Applications. Vol 3. ACM; 2019. doi:10.1145/3360550'
apa: 'Chatterjee, K., Pavlogiannis, A., & Toman, V. (2019). Value-centric dynamic
partial order reduction. In Proceedings of the 34th ACM International Conference
on Object-Oriented Programming, Systems, Languages, and Applications (Vol.
3). Athens, Greece: ACM. https://doi.org/10.1145/3360550'
chicago: Chatterjee, Krishnendu, Andreas Pavlogiannis, and Viktor Toman. “Value-Centric
Dynamic Partial Order Reduction.” In Proceedings of the 34th ACM International
Conference on Object-Oriented Programming, Systems, Languages, and Applications,
Vol. 3. ACM, 2019. https://doi.org/10.1145/3360550.
ieee: K. Chatterjee, A. Pavlogiannis, and V. Toman, “Value-centric dynamic partial
order reduction,” in Proceedings of the 34th ACM International Conference on
Object-Oriented Programming, Systems, Languages, and Applications, Athens,
Greece, 2019, vol. 3.
ista: 'Chatterjee K, Pavlogiannis A, Toman V. 2019. Value-centric dynamic partial
order reduction. Proceedings of the 34th ACM International Conference on Object-Oriented
Programming, Systems, Languages, and Applications. OOPSLA: Object-oriented Programming,
Systems, Languages and Applications vol. 3, 124.'
mla: Chatterjee, Krishnendu, et al. “Value-Centric Dynamic Partial Order Reduction.”
Proceedings of the 34th ACM International Conference on Object-Oriented Programming,
Systems, Languages, and Applications, vol. 3, 124, ACM, 2019, doi:10.1145/3360550.
short: K. Chatterjee, A. Pavlogiannis, V. Toman, in:, Proceedings of the 34th ACM
International Conference on Object-Oriented Programming, Systems, Languages, and
Applications, ACM, 2019.
conference:
end_date: 2019-10-25
location: Athens, Greece
name: 'OOPSLA: Object-oriented Programming, Systems, Languages and Applications'
start_date: 2019-10-23
date_created: 2021-10-27T14:57:06Z
date_published: 2019-10-10T00:00:00Z
date_updated: 2025-07-14T09:10:15Z
day: '10'
ddc:
- '000'
department:
- _id: GradSch
- _id: KrCh
doi: 10.1145/3360550
external_id:
arxiv:
- '1909.00989'
file:
- access_level: open_access
checksum: 2149979c46964c4d117af06ccb6c0834
content_type: application/pdf
creator: cchlebak
date_created: 2021-11-12T11:41:56Z
date_updated: 2021-11-12T11:41:56Z
file_id: '10278'
file_name: 2019_ACM_Chatterjee.pdf
file_size: 570829
relation: main_file
success: 1
file_date_updated: 2021-11-12T11:41:56Z
has_accepted_license: '1'
intvolume: ' 3'
keyword:
- safety
- risk
- reliability and quality
- software
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://dl.acm.org/doi/10.1145/3360550
month: '10'
oa: 1
oa_version: Published Version
project:
- _id: 25892FC0-B435-11E9-9278-68D0E5697425
grant_number: ICT15-003
name: Efficient Algorithms for Computer Aided Verification
- _id: 25863FF4-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S11407
name: Game Theory
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S 11407_N23
name: Rigorous Systems Engineering
- _id: 25F5A88A-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S11402-N23
name: Moderne Concurrency Paradigms
publication: Proceedings of the 34th ACM International Conference on Object-Oriented
Programming, Systems, Languages, and Applications
publication_identifier:
eissn:
- 2475-1421
publication_status: published
publisher: ACM
quality_controlled: '1'
related_material:
record:
- id: '10199'
relation: dissertation_contains
status: public
status: public
title: Value-centric dynamic partial order reduction
tmp:
image: /images/cc_by.png
legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
short: CC BY (4.0)
type: conference
user_id: 8b945eb4-e2f2-11eb-945a-df72226e66a9
volume: 3
year: '2019'
...
---
_id: '10416'
abstract:
- lang: eng
text: 'A fundamental algorithmic problem at the heart of static analysis is Dyck
reachability. The input is a graph where the edges are labeled with different
types of opening and closing parentheses, and the reachability information is
computed via paths whose parentheses are properly matched. We present new results
for Dyck reachability problems with applications to alias analysis and data-dependence
analysis. Our main contributions, that include improved upper bounds as well as
lower bounds that establish optimality guarantees, are as follows: First, we consider
Dyck reachability on bidirected graphs, which is the standard way of performing
field-sensitive points-to analysis. Given a bidirected graph with n nodes and
m edges, we present: (i) an algorithm with worst-case running time O(m + n · α(n)),
where α(n) is the inverse Ackermann function, improving the previously known O(n2)
time bound; (ii) a matching lower bound that shows that our algorithm is optimal
wrt to worst-case complexity; and (iii) an optimal average-case upper bound of
O(m) time, improving the previously known O(m · logn) bound. Second, we consider
the problem of context-sensitive data-dependence analysis, where the task is to
obtain analysis summaries of library code in the presence of callbacks. Our algorithm
preprocesses libraries in almost linear time, after which the contribution of
the library in the complexity of the client analysis is only linear, and only
wrt the number of call sites. Third, we prove that combinatorial algorithms for
Dyck reachability on general graphs with truly sub-cubic bounds cannot be obtained
without obtaining sub-cubic combinatorial algorithms for Boolean Matrix Multiplication,
which is a long-standing open problem. Thus we establish that the existing combinatorial
algorithms for Dyck reachability are (conditionally) optimal for general graphs.
We also show that the same hardness holds for graphs of constant treewidth. Finally,
we provide a prototype implementation of our algorithms for both alias analysis
and data-dependence analysis. Our experimental evaluation demonstrates that the
new algorithms significantly outperform all existing methods on the two problems,
over real-world benchmarks.'
acknowledgement: "The research was partly supported by Austrian Science Fund (FWF)
Grant No P23499-N23, FWF NFN Grant No S11407-N23 (RiSE/SHiNE), and ERC Start grant
(279307: Graph Games).\r\n"
article_number: '30'
article_processing_charge: No
article_type: original
arxiv: 1
author:
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Bhavya
full_name: Choudhary, Bhavya
last_name: Choudhary
- first_name: Andreas
full_name: Pavlogiannis, Andreas
id: 49704004-F248-11E8-B48F-1D18A9856A87
last_name: Pavlogiannis
orcid: 0000-0002-8943-0722
citation:
ama: Chatterjee K, Choudhary B, Pavlogiannis A. Optimal Dyck reachability for data-dependence
and Alias analysis. Proceedings of the ACM on Programming Languages. 2017;2(POPL).
doi:10.1145/3158118
apa: 'Chatterjee, K., Choudhary, B., & Pavlogiannis, A. (2017). Optimal Dyck
reachability for data-dependence and Alias analysis. Proceedings of the ACM
on Programming Languages. Los Angeles, CA, United States: Association for
Computing Machinery. https://doi.org/10.1145/3158118'
chicago: Chatterjee, Krishnendu, Bhavya Choudhary, and Andreas Pavlogiannis. “Optimal
Dyck Reachability for Data-Dependence and Alias Analysis.” Proceedings of the
ACM on Programming Languages. Association for Computing Machinery, 2017. https://doi.org/10.1145/3158118.
ieee: K. Chatterjee, B. Choudhary, and A. Pavlogiannis, “Optimal Dyck reachability
for data-dependence and Alias analysis,” Proceedings of the ACM on Programming
Languages, vol. 2, no. POPL. Association for Computing Machinery, 2017.
ista: Chatterjee K, Choudhary B, Pavlogiannis A. 2017. Optimal Dyck reachability
for data-dependence and Alias analysis. Proceedings of the ACM on Programming
Languages. 2(POPL), 30.
mla: Chatterjee, Krishnendu, et al. “Optimal Dyck Reachability for Data-Dependence
and Alias Analysis.” Proceedings of the ACM on Programming Languages, vol.
2, no. POPL, 30, Association for Computing Machinery, 2017, doi:10.1145/3158118.
short: K. Chatterjee, B. Choudhary, A. Pavlogiannis, Proceedings of the ACM on Programming
Languages 2 (2017).
conference:
end_date: 2018-01-13
location: Los Angeles, CA, United States
name: 'POPL: Programming Languages'
start_date: 2018-01-07
date_created: 2021-12-05T23:01:48Z
date_published: 2017-12-27T00:00:00Z
date_updated: 2023-02-23T12:27:13Z
day: '27'
ddc:
- '000'
department:
- _id: KrCh
doi: 10.1145/3158118
ec_funded: 1
external_id:
arxiv:
- '1910.00241'
file:
- access_level: open_access
checksum: faa3f7b3fe8aab84b50ed805c26a0ee5
content_type: application/pdf
creator: cchlebak
date_created: 2021-12-07T08:06:28Z
date_updated: 2021-12-07T08:06:28Z
file_id: '10421'
file_name: 2017_ACMProgLang_Chatterjee.pdf
file_size: 460188
relation: main_file
success: 1
file_date_updated: 2021-12-07T08:06:28Z
has_accepted_license: '1'
intvolume: ' 2'
issue: POPL
language:
- iso: eng
month: '12'
oa: 1
oa_version: Published Version
project:
- _id: 2581B60A-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '279307'
name: 'Quantitative Graph Games: Theory and Applications'
- _id: 2584A770-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: P 23499-N23
name: Modern Graph Algorithmic Techniques in Formal Verification
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S 11407_N23
name: Rigorous Systems Engineering
publication: Proceedings of the ACM on Programming Languages
publication_identifier:
eissn:
- 2475-1421
publication_status: published
publisher: Association for Computing Machinery
quality_controlled: '1'
related_material:
record:
- id: '5455'
relation: earlier_version
status: public
scopus_import: '1'
status: public
title: Optimal Dyck reachability for data-dependence and Alias analysis
tmp:
image: /images/cc_by.png
legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
short: CC BY (4.0)
type: journal_article
user_id: 8b945eb4-e2f2-11eb-945a-df72226e66a9
volume: 2
year: '2017'
...
---
_id: '10417'
abstract:
- lang: eng
text: "We present a new dynamic partial-order reduction method for stateless model
checking of concurrent programs. A common approach for exploring program behaviors
relies on enumerating the traces of the program, without storing the visited states
(aka stateless exploration). As the number of distinct traces grows exponentially,
dynamic partial-order reduction (DPOR) techniques have been successfully used
to partition the space of traces into equivalence classes (Mazurkiewicz partitioning),
with the goal of exploring only few representative traces from each class.\r\n\r\nWe
introduce a new equivalence on traces under sequential consistency semantics,
which we call the observation equivalence. Two traces are observationally equivalent
if every read event observes the same write event in both traces. While the traditional
Mazurkiewicz equivalence is control-centric, our new definition is data-centric.
We show that our observation equivalence is coarser than the Mazurkiewicz equivalence,
and in many cases even exponentially coarser. We devise a DPOR exploration of
the trace space, called data-centric DPOR, based on the observation equivalence."
acknowledgement: "The research was partly supported by Austrian Science Fund (FWF)
Grant No P23499- N23, FWF\r\nNFN Grant No S11407-N23 (RiSE/SHiNE), ERC Start grant
(279307: Graph Games), and Czech\r\nScience Foundation grant GBP202/12/G061."
article_number: '31'
article_processing_charge: No
article_type: original
arxiv: 1
author:
- first_name: Marek
full_name: Chalupa, Marek
last_name: Chalupa
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Andreas
full_name: Pavlogiannis, Andreas
id: 49704004-F248-11E8-B48F-1D18A9856A87
last_name: Pavlogiannis
orcid: 0000-0002-8943-0722
- first_name: Nishant
full_name: Sinha, Nishant
last_name: Sinha
- first_name: Kapil
full_name: Vaidya, Kapil
last_name: Vaidya
citation:
ama: Chalupa M, Chatterjee K, Pavlogiannis A, Sinha N, Vaidya K. Data-centric dynamic
partial order reduction. Proceedings of the ACM on Programming Languages.
2017;2(POPL). doi:10.1145/3158119
apa: 'Chalupa, M., Chatterjee, K., Pavlogiannis, A., Sinha, N., & Vaidya, K.
(2017). Data-centric dynamic partial order reduction. Proceedings of the ACM
on Programming Languages. Los Angeles, CA, United States: Association for
Computing Machinery. https://doi.org/10.1145/3158119'
chicago: Chalupa, Marek, Krishnendu Chatterjee, Andreas Pavlogiannis, Nishant Sinha,
and Kapil Vaidya. “Data-Centric Dynamic Partial Order Reduction.” Proceedings
of the ACM on Programming Languages. Association for Computing Machinery,
2017. https://doi.org/10.1145/3158119.
ieee: M. Chalupa, K. Chatterjee, A. Pavlogiannis, N. Sinha, and K. Vaidya, “Data-centric
dynamic partial order reduction,” Proceedings of the ACM on Programming Languages,
vol. 2, no. POPL. Association for Computing Machinery, 2017.
ista: Chalupa M, Chatterjee K, Pavlogiannis A, Sinha N, Vaidya K. 2017. Data-centric
dynamic partial order reduction. Proceedings of the ACM on Programming Languages.
2(POPL), 31.
mla: Chalupa, Marek, et al. “Data-Centric Dynamic Partial Order Reduction.” Proceedings
of the ACM on Programming Languages, vol. 2, no. POPL, 31, Association for
Computing Machinery, 2017, doi:10.1145/3158119.
short: M. Chalupa, K. Chatterjee, A. Pavlogiannis, N. Sinha, K. Vaidya, Proceedings
of the ACM on Programming Languages 2 (2017).
conference:
end_date: 2018-01-13
location: Los Angeles, CA, United States
name: 'POPL: Programming Languages'
start_date: 2018-01-07
date_created: 2021-12-05T23:01:49Z
date_published: 2017-12-27T00:00:00Z
date_updated: 2023-02-23T12:27:16Z
day: '27'
department:
- _id: KrCh
doi: 10.1145/3158119
ec_funded: 1
external_id:
arxiv:
- '1610.01188'
intvolume: ' 2'
issue: POPL
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://dl.acm.org/doi/10.1145/3158119
month: '12'
oa: 1
oa_version: Published Version
project:
- _id: 2584A770-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: P 23499-N23
name: Modern Graph Algorithmic Techniques in Formal Verification
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S 11407_N23
name: Rigorous Systems Engineering
- _id: 2581B60A-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '279307'
name: 'Quantitative Graph Games: Theory and Applications'
publication: Proceedings of the ACM on Programming Languages
publication_identifier:
eissn:
- 2475-1421
publication_status: published
publisher: Association for Computing Machinery
quality_controlled: '1'
related_material:
record:
- id: '5448'
relation: earlier_version
status: public
- id: '5456'
relation: earlier_version
status: public
scopus_import: '1'
status: public
title: Data-centric dynamic partial order reduction
type: journal_article
user_id: 8b945eb4-e2f2-11eb-945a-df72226e66a9
volume: 2
year: '2017'
...
---
_id: '10418'
abstract:
- lang: eng
text: We present a new proof rule for proving almost-sure termination of probabilistic
programs, including those that contain demonic non-determinism. An important question
for a probabilistic program is whether the probability mass of all its diverging
runs is zero, that is that it terminates "almost surely". Proving that can be
hard, and this paper presents a new method for doing so. It applies directly to
the program's source code, even if the program contains demonic choice. Like others,
we use variant functions (a.k.a. "super-martingales") that are real-valued and
decrease randomly on each loop iteration; but our key innovation is that the amount
as well as the probability of the decrease are parametric. We prove the soundness
of the new rule, indicate where its applicability goes beyond existing rules,
and explain its connection to classical results on denumerable (non-demonic) Markov
chains.
acknowledgement: "McIver and Morgan are grateful to David Basin and the Information
Security Group at ETH Zürich for hosting a six-month stay in Switzerland, during
part of which this work began. And thanks particularly to Andreas Lochbihler, who
shared with us the probabilistic termination problem that led to it. They acknowledge
the support of ARC grant DP140101119. Part of this work was carried out during the
Workshop on Probabilistic Programming Semantics\r\nat McGill University’s Bellairs
Research Institute on Barbados organised by Alexandra Silva and\r\nPrakash Panangaden.
Kaminski and Katoen are grateful to Sebastian Junges for spotting a flaw in §5.4."
article_number: '33'
article_processing_charge: No
article_type: original
arxiv: 1
author:
- first_name: Annabelle
full_name: Mciver, Annabelle
last_name: Mciver
- first_name: Carroll
full_name: Morgan, Carroll
last_name: Morgan
- first_name: Benjamin Lucien
full_name: Kaminski, Benjamin Lucien
last_name: Kaminski
- first_name: Joost P
full_name: Katoen, Joost P
id: 4524F760-F248-11E8-B48F-1D18A9856A87
last_name: Katoen
citation:
ama: Mciver A, Morgan C, Kaminski BL, Katoen JP. A new proof rule for almost-sure
termination. Proceedings of the ACM on Programming Languages. 2017;2(POPL).
doi:10.1145/3158121
apa: 'Mciver, A., Morgan, C., Kaminski, B. L., & Katoen, J. P. (2017). A new
proof rule for almost-sure termination. Proceedings of the ACM on Programming
Languages. Los Angeles, CA, United States: Association for Computing Machinery.
https://doi.org/10.1145/3158121'
chicago: Mciver, Annabelle, Carroll Morgan, Benjamin Lucien Kaminski, and Joost
P Katoen. “A New Proof Rule for Almost-Sure Termination.” Proceedings of the
ACM on Programming Languages. Association for Computing Machinery, 2017. https://doi.org/10.1145/3158121.
ieee: A. Mciver, C. Morgan, B. L. Kaminski, and J. P. Katoen, “A new proof rule
for almost-sure termination,” Proceedings of the ACM on Programming Languages,
vol. 2, no. POPL. Association for Computing Machinery, 2017.
ista: Mciver A, Morgan C, Kaminski BL, Katoen JP. 2017. A new proof rule for almost-sure
termination. Proceedings of the ACM on Programming Languages. 2(POPL), 33.
mla: Mciver, Annabelle, et al. “A New Proof Rule for Almost-Sure Termination.” Proceedings
of the ACM on Programming Languages, vol. 2, no. POPL, 33, Association for
Computing Machinery, 2017, doi:10.1145/3158121.
short: A. Mciver, C. Morgan, B.L. Kaminski, J.P. Katoen, Proceedings of the ACM
on Programming Languages 2 (2017).
conference:
end_date: 2018-01-13
location: Los Angeles, CA, United States
name: 'POPL: Programming Languages'
start_date: 2018-01-07
date_created: 2021-12-05T23:01:49Z
date_published: 2017-12-07T00:00:00Z
date_updated: 2021-12-07T08:04:14Z
day: '07'
department:
- _id: KrCh
- _id: ToHe
doi: 10.1145/3158121
external_id:
arxiv:
- '1711.03588'
intvolume: ' 2'
issue: POPL
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://dl.acm.org/doi/10.1145/3158121
month: '12'
oa: 1
oa_version: Published Version
publication: Proceedings of the ACM on Programming Languages
publication_identifier:
eissn:
- 2475-1421
publication_status: published
publisher: Association for Computing Machinery
quality_controlled: '1'
scopus_import: '1'
status: public
title: A new proof rule for almost-sure termination
type: journal_article
user_id: 8b945eb4-e2f2-11eb-945a-df72226e66a9
volume: 2
year: '2017'
...