Deadlock in packet switching networks

Anna Stramaglia; Jeroen J. A. Keiren; Hans Zantema

Deadlock in packet switching networks

Anna Stramaglia, Jeroen J. A. Keiren, Hans Zantema

Research output: Working paper › Preprint › Academic

27 Downloads (Pure)

Abstract

A deadlock in a packet switching network is a state in which one or more messages have not yet reached their target, yet cannot progress any further. We formalize three different notions of deadlock in the context of packet switching networks, to which we refer as global, local and weak deadlock. We establish the precise relations between these notions, and prove they characterize different sets of deadlocks. Moreover, we implement checking of deadlock freedom of packet switching networks using the symbolic model checker nuXmv. We show experimentally that the implementation is effective at finding subtle deadlock situations in packet switching networks.

Original language	English
Volume	abs/2101.06015
Publication status	Published - 15 Jan 2021

Publication series

Name	CoRR
Publisher	Schloss Dagstuhl - Leibniz-Zentrum für Informatik
ISSN (Print)	2331-8422

Bibliographical note

This is a version with full proofs of the preprint that was submitted to FSEN 2021, and accepted for publication in that conference (published in Springer LNCS)

Keywords

cs.NI
cs.LO

Access to Document

2101.06015v1

1 Conference contribution

Deadlock in Packet Switching Networks
Stramaglia, A., Keiren, J. J. A. & Zantema, H., 17 Oct 2021, Fundamentals of Software Engineering - 9th International Conference, FSEN 2021, Virtual Event, May 19-21, 2021, Revised Selected Papers. Hojjat, H. & Massink, M. (eds.). Springer, p. 127-141 15 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 12818 LNCS).
Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

Cite this

@techreport{6e6c6e25ffb94192a8e4a4debaff52a0,

title = "Deadlock in packet switching networks",

abstract = " A deadlock in a packet switching network is a state in which one or more messages have not yet reached their target, yet cannot progress any further. We formalize three different notions of deadlock in the context of packet switching networks, to which we refer as global, local and weak deadlock. We establish the precise relations between these notions, and prove they characterize different sets of deadlocks. Moreover, we implement checking of deadlock freedom of packet switching networks using the symbolic model checker nuXmv. We show experimentally that the implementation is effective at finding subtle deadlock situations in packet switching networks. ",

keywords = "cs.NI, cs.LO",

author = "Anna Stramaglia and Keiren, {Jeroen J. A.} and Hans Zantema",

note = "This is a version with full proofs of the preprint that was submitted to FSEN 2021, and accepted for publication in that conference (published in Springer LNCS)",

year = "2021",

month = jan,

day = "15",

language = "English",

volume = "abs/2101.06015",

series = "CoRR",

publisher = "Schloss Dagstuhl - Leibniz-Zentrum f{\"u}r Informatik",

type = "WorkingPaper",

institution = "Schloss Dagstuhl - Leibniz-Zentrum f{\"u}r Informatik",

}

TY - UNPB

T1 - Deadlock in packet switching networks

AU - Stramaglia, Anna

AU - Keiren, Jeroen J. A.

AU - Zantema, Hans

N1 - This is a version with full proofs of the preprint that was submitted to FSEN 2021, and accepted for publication in that conference (published in Springer LNCS)

PY - 2021/1/15

Y1 - 2021/1/15

N2 - A deadlock in a packet switching network is a state in which one or more messages have not yet reached their target, yet cannot progress any further. We formalize three different notions of deadlock in the context of packet switching networks, to which we refer as global, local and weak deadlock. We establish the precise relations between these notions, and prove they characterize different sets of deadlocks. Moreover, we implement checking of deadlock freedom of packet switching networks using the symbolic model checker nuXmv. We show experimentally that the implementation is effective at finding subtle deadlock situations in packet switching networks.

AB - A deadlock in a packet switching network is a state in which one or more messages have not yet reached their target, yet cannot progress any further. We formalize three different notions of deadlock in the context of packet switching networks, to which we refer as global, local and weak deadlock. We establish the precise relations between these notions, and prove they characterize different sets of deadlocks. Moreover, we implement checking of deadlock freedom of packet switching networks using the symbolic model checker nuXmv. We show experimentally that the implementation is effective at finding subtle deadlock situations in packet switching networks.

KW - cs.NI

KW - cs.LO

M3 - Preprint

VL - abs/2101.06015

T3 - CoRR

BT - Deadlock in packet switching networks

ER -

Deadlock in packet switching networks

Abstract

Publication series

Bibliographical note

Keywords

Access to Document

Fingerprint

Research output

Deadlock in Packet Switching Networks

Cite this