Deadlock in packet switching networks

DOI10.1007/978-3-030-89247-0_9zbMATH Open1496.68043arXiv2101.06015OpenAlexW3208964046MaRDI QIDQ2145272FDOQ2145272

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

Publication date: 17 June 2022

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.

Full work available at URL: https://arxiv.org/abs/2101.06015

Recommendations

• Predicting deadlock in store‐and‐forward networks
• A deadlock free and starvation free network of packet switching communication processors
• Deadlock analysis in networks of communicating processes
• scientific article; zbMATH DE number 3926230
• A simple livelock-free algorithm for packet switching

zbMATH Keywords

model checkingdeadlockpacket switching network

Mathematics Subject Classification ID

Performance evaluation, queueing, and scheduling in the context of computer systems (68M20) Specification and verification (program logics, model checking, etc.) (68Q60) Network design and communication in computer systems (68M10)

Cites Work

• Title not available (Why is that?)
• Deadlock-Free Packet Switching Networks
• Title not available (Why is that?)

Cited In (4)

• Title not available (Why is that?)
• Characterization of deadlocks in irregular networks
• Correct Hardware Design and Verification Methods
• A deadlock free and starvation free network of packet switching communication processors

Uses Software

• ACL2
• nuXmv

This page was built for publication: Deadlock in packet switching networks

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2145272)