Interleaving & Reconfigurable Interaction: Separating Choice from Scheduling using Glue

TL;DR

This paper introduces glued partial orders to model reconfigurable interactions in concurrent systems, effectively separating choice from scheduling and capturing all possible behaviors including reconfiguration.

Contribution

It proposes glued partial orders as a novel method to represent reconfiguration in concurrent systems, extending partial order semantics to handle nondeterminism caused by reconfiguration.

Findings

Glued partial orders accurately model reconfiguration effects.

They distinguish between nondeterministic choices and scheduling.

The approach captures all partial order computations with reconfiguration.

Abstract

Reconfigurable interaction induces another dimension of nondeterminism in concurrent systems which makes it hard to reason about the different choices of the system from a global perspective. Namely, (1) choices that correspond to concurrent execution of independent events; and (2) forced interleaving (or scheduling) due to reconfiguration. Unlike linear order semantics of computations, partial order semantics recovers information about the interdependence among the different events for fixed interaction, but still is unable to handle reconfiguration. We introduce glued partial orders as a way to capture reconfiguration. Much like partial orders capture all possible choices for fixed systems, glued partial orders capture all possible choices alongside reconfiguration. We show that a glued partial order is sufficient to correctly capture all partial order computations that differ in forced interleaving due to reconfiguration. Furthermore, we show that computations belonging to different glued partial orders are only different due to non-determinism.