On the Preservation of Properties when Changing Communication Models Olav Bunte1 Louis C.M. van Gool2 and Tim A.C. Willemse1

2025-04-27 0 0 660.11KB 26 页 10玖币

侵权投诉

On the Preservation of Properties when Changing

Communication Models ?

Olav Bunte1, Louis C.M. van Gool2, and Tim A.C. Willemse1

1Eindhoven University of Technology, Eindhoven, Netherlands

{o.bunte, t.a.c.willemse}@tue.nl

2Canon Production Printing, Venlo, Netherlands

louis.vangool@cpp.canon

Abstract. In a system of processes that communicate asynchronously

by means of FIFO channels, there are many options in which these chan-

nels can be laid out. In this paper, we compare channel layouts in how

they aﬀect the behaviour of the system using an ordering based on split-

ting and merging channels. This order induces a simulation relation,

from which the preservation of safety properties follows. Also, we iden-

tify conditions under which the properties reachability, deadlock freedom

and conﬂuence are preserved when changing the channel layout.

Keywords: Asynchronous communication ·Communication models ·

Property preservation ·Conﬂuence

1 Introduction

In asynchronous communication, sending and receiving a message are two sep-

arate actions, which makes it possible for messages to be received in a diﬀer-

ent order than they were sent. What orderings are possible, depends on the

asynchronous communication model(s) used within the system, for which many

ﬂavours are possible. We consider communication models that are implemented

by means of a layout of (unbounded) FIFO (First In First Out) channels, which

deﬁnes how messages in transit are stored. For instance, using a channel per

message implements a fully asynchronous model, while having a single input

channel per process enforces that messages that are sent to the same process are

received in the same order in which they are sent.

While (re)designing or refactoring a software system of asynchronously com-

municating processes, it may be desirable to change (part of) the channel layout.

This can, for instance, be the case when design choices are still being explored,

when the performance of the system needs to be improved, when the behaviour

of the system has grown too complex due to the additions of new processes, or

when the channel implementation is part of legacy software. However, changing

the channel layout may impact the behaviour of the system in unexpected ways,

?This work was carried out as part of the VOICE-B project, which is funded by Canon

Production Printing.

arXiv:2210.06196v1 [cs.LO] 12 Oct 2022

2 O. Bunte et al.

possibly violating desired properties. In this paper, we investigate the extent of

this impact.

We use the notion of a FIFO system [FP20,BFS20] to represent a software

system of asynchronously communicating processes. Firstly, we deﬁne an order-

ing on FIFO systems based on whether one can be created from the other by

merging channels. We then analyse the diﬀerence in the behaviour between re-

lated FIFO systems and show that it induces a simulation order, from which the

preservation of safety properties follows. Secondly, we analyse whether reacha-

bility, deadlock freedom and conﬂuence are preserved when changing the chan-

nel layout. Reachability is particularly relevant in practice, since changing the

method of communication should typically not cause previously possible process

behaviour to become impossible. If deadlock freedom is preserved, it is ensured

that changing the method of communication does not introduce undesired situ-

ations where all processes are stuck waiting for each other. Conﬂuence is related

to the independence of actions, which is often expected between actions of dif-

ferent processes. A violation of conﬂuence between actions of diﬀerent processes

indicates a possible race condition, where the faster process determines how

the system progresses. We identify conditions under which these properties are

guaranteed to be preserved when merging or splitting channels.

Related work. In [EMR02], seven distinct channel-based asynchronous commu-

nication models are related to each other in a hierarchy based on trace and MSC

implementability. The authors of [CHQ16] also consider the causal communica-

tion model [Lam78], and show a similar hierarchy. They prove this hierarchy cor-

rect in [CHNQ19] using automated proof techniques. Compared to these works,

we consider mixed (channel-based) communication models, which is more realis-

tic for complex software systems. For communication models that can be deﬁned

by FIFO systems, the hierarchies in these works relate these models the same

way as our relation does.

Property preservation is closely related to the ﬁeld of incremental model

checking [SS94,HJMS03,WE13], which is an eﬃcient method for rechecking a

property on a system that has undergone some changes. Under some conditions,

one can actually prove that a property will be preserved, as shown in multiple

contexts [LGS+95,Weh00,HVG03,DS12,XL21]. To our knowledge, no such work

exists in the context of asynchronously communicating processes however.

Outline. We ﬁrst introduce the necessary deﬁnitions to reason about FIFO sys-

tems in Section 2. We deﬁne an ordering between FIFO systems in Section 3and

show that it induces a simulation relation. Then in Section 4we identify condi-

tions under which the aforementioned properties are preserved when changing

the channel layout. Lastly, we conclude in Section 5. The proofs for all lemmas

and theorems in Section 3and 4can be found in the Appendix.

On the Preservation of Properties when Changing Communication Models 3

2 The FIFO system

Let Pbe a set of processes that make up a software system and let Mbe

the set of messages that can be communicated between these processes. We

represent the behaviour of each process p∈Pwith a Labelled Transition System

(LTS) Bp=hQp, q0

p, Lp,−_piwhere Qpis its set of states, q0

pits initial state,

Lp⊆({?,!} × M)∪ {τ}its set of actions and −_p⊆Qp×Lp×Qpits transition

relation. An action ?mindicates the receiving of m,!mthe sending of mand

τis an internal action. We assume that processes do not share non-internal

actions, that is Lp∩Lp0⊆ {τ}for all distinct p, p0∈P. We write qa

−_pq0iﬀ

(q, a, q0)∈ −_p. A FIFO system then describes how these processes communicate

with each other via FIFO channels.

Deﬁnition 1. AFIFO system is a tuple hP, C, M iwhere C⊆ P(M)is a set of

(FIFO) channels deﬁned as a partition of M.

Each channel in Cis deﬁned as a set of messages, which represents the

messages that this channel can hold. Note that because Cpartitions M, we

assume that each message can only be sent to and received from exactly one

channel. For a message m∈M, we deﬁne [m]Cas the channel in Cthat m

belongs to, that is m∈[m]Cand [m]C∈C. We write m'Coiﬀ [m]C= [o]C

for messages m, o ∈M.

We deﬁne M∗as the set of all ﬁnite sequences of messages, also known as

words. We use as the empty word and concatenate two words with ++. Given

a word m++ wfor message m∈Mand word w∈M∗, we deﬁne its head as

hd(m++ w) = mand its tail as tl(m++ w) = w.

Example 1. Imagine two vending machines, one for healthy snacks and one for

unhealthy snacks, and some user who can interact with these vending machines.

After receiving a "healthy voucher" , the healthy vending machine can sup-

ply apples and bananas . After receiving an "unhealthy voucher" , the

unhealthy vending machine can supply chocolate and donuts . The user

decides to use before and can receive the snacks whenever they are ready.

Let PV={hvm, uvm, user}be processes that represent the two vending

machines and the user. Their LTSs are visualised in Figure 1. The set of mes-

sages is MV={, , , , , }. The realistic case where both vending

hvm :0 1 2 3

? ! ! uvm :0 1 2 3

? ! !

user :012

?,?

!?,?,?,?

Fig. 1: Processes hvm,uvm and user for Example 1and 2.

4 O. Bunte et al.

machines have their own voucher slot and output slot is represented by the

channel set CV={{ },{ },{,},{,}}, resulting in the FIFO system

hPV, CV, MVi. Note that 'CVand 'CV.

Semantics A FIFO system induces an LTS that represents the communication

behaviour between all processes. A state in this LTS consists of two parts: the

states of the individual processes and the contents of the channels. For a set of

processes P,P={κ∈P→Sp∈PQp| ∀p∈P:κ(p)∈Qp}denotes the set of

functions that map processes to their current states. For a set of channels C,

C={ζ∈C→M∗| ∀c∈C:ζ(c)∈c∗}denotes the set of functions that map

channels to their contents. In case of a set of channels C0, we write C0. Note that

we assume unbounded channels.

Deﬁnition 2. Let F=h(Qp, q0

p,−_p)p∈P, C, M ibe a FIFO system. The seman-

tics of Fis an LTS BF=hS, s0, L, −→i where

–S=P×C,

–s0= (κ0, ζ), where κ0(p) = q0

pfor all p∈Pand ζ(c) = for all c∈C,

–L= ({?,!} × M)∪ {τ},

–−→ ⊆ S×L×Ssuch that for all (κ, ζ)∈S,p∈P,q∈Qpand m∈M, with

c= [m]C:

(κ, ζ)τ

−→ (κ[p7→ q], ζ)iﬀ κ(p)τ

−_pq

(κ, ζ)?m

−−→ (κ[p7→ q], ζ[c7→ tl(ζ(c)]) iﬀ κ(p)?m

−−_pq∧hd(ζ(c)) = m

(κ, ζ)!m

−−→ (κ[p7→ q], ζ[c7→ ζ(c) ++ m]) iﬀ κ(p)!m

−−_pq

We write sa

−→ s0iﬀ (s, a, s0)∈ −→. We lift the transition relation to one over

sequences of actions −→∗⊆S×L∗×Sin the usual way. In the context of a FIFO

system F, we refer to the semantics of the FIFO system as deﬁned above as “the

LTS of F”.

Two LTSs can be compared by means of a simulation relation [LGS+95].

Deﬁnition 3. Let B=hS, s0, L, −→i and B0=hS0, s0

0, L, −→0ibe two LTSs. We

say that Bsimulates B0iﬀ there exists a simulation relation R⊆S0×Ssuch

that s0

0Rs0and for all s∈Sand s0∈S0, if s0Rs and s0a

−→0t0for some t0∈S0

and a∈L, then there must exist a t∈Ssuch that sa

−→ tand t0Rt.

3 Comparing channel layouts

The choice in channel layout aﬀects the behaviour of a FIFO system. The more

channels there are, the more orderings there are in which messages can be re-

ceived. With this in mind, we order FIFO systems as follows:

Deﬁnition 4. Let F=hP, C, M iand F0=hP, C0, M ibe two FIFO systems.

We deﬁne the relation on FIFO systems such that FF0iﬀ C6=C0and

∀c∈C:∃c0∈C0:c⊆c0(that is, Cis a more reﬁned partition of Mthan C0is).

On the Preservation of Properties when Changing Communication Models 5

One can create F0from Fby merging a number of channels (splitting chan-

nels in the opposite direction). We ﬁrst illustrate how this aﬀects the behaviour

of the system with an example.

Example 2. Continuing from Example 1, consider the FIFO systems Fm=

hPV,{{ },{ },{ },{ },{ },{ }}, MVi(one channel per message), Fo=

hPV,{{ ,},{,},{,}}, MVi(one output channel per process) and

Fg=hPV,{MV}, MVi(one global channel). Observe that FmFoFg.

In Fm, the trace ! ! ? is possible, but in Foit is not. This is because

in Fo, both vouchers sent by user are put in the same channel, so hvm has to

receive its voucher before uvm can. In Fo, the trace ! ! ? ? ! ! ? is

possible, but in Fgit is not. This is because in Fg, both vending machines send

their snacks to the same channel, which ﬁxes the order in which user receives

the snacks.

In the remainder of this section, to avoid duplication in deﬁnitions, lem-

mas and theorems, we universally quantify over FIFO systems F=hP, C, M i

and F0=hP, C0, M isuch that FF0, with BF=hS, s0, L, −→i and BF0=

hS0, s0

0, L, −→0i.

The eﬀect on the LTS when changing the channel layout is visualised in

Figure 2. When the channels {m}and {o}are merged into one channel {m, o},

state sresults in states s1and s2, one for every interleaving of the contents of

the two channels in s. Conversely, when channel {m, o}is split into channels

{m}and {o}, the channel contents of states s1and s2are split as well, making

them coincide, resulting in s. We say that state sgeneralises states s1and s2

and that states s1and s2specialise state s.

To deﬁne this formally, we ﬁrst deﬁne the interleavings of words. Given a

message m∈Mand a set of words W, let m++ W={m++ w|w∈W}. Then

for a set of words W, we deﬁne the set of possible interleavings of these words

Was

W={}if W={}, else

W=Sm++w∈Wm++

((W\{m++w})∪{w}).

Example 3. Continuing from Example 2, let W={, , }. Then ||W=

{,,,,,}.

With this, we can deﬁne generalisation/specialisation of states as follows:

smo

!o?m

!m?o

merging

splitting

Fig. 2: A visualisation of the eﬀect on the LTS of a FIFO system when merging

or splitting channels. Transitions without a label cover any transition that is not

already represented by other incoming or outgoing transitions.

文档加载中……请稍候！
如果长时间未打开，您也可以点击刷新试试。

下载文档到电脑，查找使用更方便

10 玖币 0人已下载

立即下载

摘要：

OnthePreservationofPropertieswhenChangingCommunicationModels?OlavBunte1,LouisC.M.vanGool2,andTimA.C.Willemse11EindhovenUniversityofTechnology,Eindhoven,Netherlands{o.bunte,t.a.c.willemse}@tue.nl2CanonProductionPrinting,Venlo,Netherlandslouis.vangool@cpp.canonAbstract.Inasystemofprocessesthatcommunic...

展开>> 收起<<

On the Preservation of Properties when Changing Communication Models Olav Bunte1 Louis C.M. van Gool2 and Tim A.C. Willemse1.pdf

共26页,预览5页

还剩页未读，继续阅读

声明：本站为文档C2C交易模式，即用户上传的文档直接被用户下载，本站只是中间服务平台，本站所有文档下载所得的收益归上传人(含作者)所有。玖贝云文库仅提供信息存储空间，仅对用户上传内容的表现方式做保护处理，对上载内容本身不做任何修改或编辑。若文档所含内容侵犯了您的版权或隐私，请立即通知玖贝云文库，我们立即给予删除！

On the Preservation of Properties when Changing Communication Models Olav Bunte1 Louis C.M. van Gool2 and Tim A.C. Willemse1

相关推荐

开通VIP享超值会员特权

作者详情

相关内容

热门标签

举报选择: