---
_id: '10855'
abstract:
- lang: eng
text: 'Consider a distributed task where the communication network is fixed but
the local inputs given to the nodes of the distributed system may change over
time. In this work, we explore the following question: if some of the local inputs
change, can an existing solution be updated efficiently, in a dynamic and distributed
manner? To address this question, we define the batch dynamic \congest model in
which we are given a bandwidth-limited communication network and a dynamic edge
labelling defines the problem input. The task is to maintain a solution to a graph
problem on the labeled graph under batch changes. We investigate, when a batch
of α edge label changes arrive, \beginitemize \item how much time as a function
of α we need to update an existing solution, and \item how much information the
nodes have to keep in local memory between batches in order to update the solution
quickly. \enditemize Our work lays the foundations for the theory of input-dynamic
distributed network algorithms. We give a general picture of the complexity landscape
in this model, design both universal algorithms and algorithms for concrete problems,
and present a general framework for lower bounds. In particular, we derive non-trivial
upper bounds for two selected, contrasting problems: maintaining a minimum spanning
tree and detecting cliques.'
acknowledgement: "We thank Jukka Suomela for discussions. We also thank our shepherd
Mohammad Hajiesmaili\r\nand the reviewers for their time and suggestions on how
to improve the paper. This project\r\nhas received funding from the European Research
Council (ERC) under the European Union’s\r\nHorizon 2020 research and innovation
programme (grant agreement No 805223 ScaleML), from the European Union’s Horizon
2020 research and innovation programme under the Marie\r\nSk lodowska–Curie grant
agreement No. 840605, from the Vienna Science and Technology Fund (WWTF) project
WHATIF, ICT19-045, 2020-2024, and from the Austrian Science Fund (FWF) and netIDEE
SCIENCE project P 33775-N."
article_processing_charge: No
article_type: original
arxiv: 1
author:
- first_name: Klaus-Tycho
full_name: Foerster, Klaus-Tycho
last_name: Foerster
- first_name: Janne
full_name: Korhonen, Janne
id: C5402D42-15BC-11E9-A202-CA2BE6697425
last_name: Korhonen
- first_name: Ami
full_name: Paz, Ami
last_name: Paz
- first_name: Joel
full_name: Rybicki, Joel
id: 334EFD2E-F248-11E8-B48F-1D18A9856A87
last_name: Rybicki
orcid: 0000-0002-6432-6646
- first_name: Stefan
full_name: Schmid, Stefan
last_name: Schmid
citation:
ama: Foerster K-T, Korhonen J, Paz A, Rybicki J, Schmid S. Input-dynamic distributed
algorithms for communication networks. Proceedings of the ACM on Measurement
and Analysis of Computing Systems. 2021;5(1):1-33. doi:10.1145/3447384
apa: Foerster, K.-T., Korhonen, J., Paz, A., Rybicki, J., & Schmid, S. (2021).
Input-dynamic distributed algorithms for communication networks. Proceedings
of the ACM on Measurement and Analysis of Computing Systems. Association for
Computing Machinery. https://doi.org/10.1145/3447384
chicago: Foerster, Klaus-Tycho, Janne Korhonen, Ami Paz, Joel Rybicki, and Stefan
Schmid. “Input-Dynamic Distributed Algorithms for Communication Networks.” Proceedings
of the ACM on Measurement and Analysis of Computing Systems. Association for
Computing Machinery, 2021. https://doi.org/10.1145/3447384.
ieee: K.-T. Foerster, J. Korhonen, A. Paz, J. Rybicki, and S. Schmid, “Input-dynamic
distributed algorithms for communication networks,” Proceedings of the ACM
on Measurement and Analysis of Computing Systems, vol. 5, no. 1. Association
for Computing Machinery, pp. 1–33, 2021.
ista: Foerster K-T, Korhonen J, Paz A, Rybicki J, Schmid S. 2021. Input-dynamic
distributed algorithms for communication networks. Proceedings of the ACM on Measurement
and Analysis of Computing Systems. 5(1), 1–33.
mla: Foerster, Klaus-Tycho, et al. “Input-Dynamic Distributed Algorithms for Communication
Networks.” Proceedings of the ACM on Measurement and Analysis of Computing
Systems, vol. 5, no. 1, Association for Computing Machinery, 2021, pp. 1–33,
doi:10.1145/3447384.
short: K.-T. Foerster, J. Korhonen, A. Paz, J. Rybicki, S. Schmid, Proceedings of
the ACM on Measurement and Analysis of Computing Systems 5 (2021) 1–33.
date_created: 2022-03-18T09:10:27Z
date_published: 2021-03-01T00:00:00Z
date_updated: 2023-09-26T10:40:55Z
day: '01'
department:
- _id: DaAl
doi: 10.1145/3447384
ec_funded: 1
external_id:
arxiv:
- '2005.07637'
intvolume: ' 5'
issue: '1'
keyword:
- Computer Networks and Communications
- Hardware and Architecture
- Safety
- Risk
- Reliability and Quality
- Computer Science (miscellaneous)
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://arxiv.org/abs/2005.07637
month: '03'
oa: 1
oa_version: Preprint
page: 1-33
project:
- _id: 26A5D39A-B435-11E9-9278-68D0E5697425
call_identifier: H2020
grant_number: '840605'
name: Coordination in constrained and natural distributed systems
- _id: 268A44D6-B435-11E9-9278-68D0E5697425
call_identifier: H2020
grant_number: '805223'
name: Elastic Coordination for Scalable Machine Learning
publication: Proceedings of the ACM on Measurement and Analysis of Computing Systems
publication_identifier:
issn:
- 2476-1249
publication_status: published
publisher: Association for Computing Machinery
quality_controlled: '1'
related_material:
record:
- id: '10854'
relation: shorter_version
status: public
scopus_import: '1'
status: public
title: Input-dynamic distributed algorithms for communication networks
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
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: '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'
...