Follow with Edit this page on Go back to the Bliki index

Knowledge of Choice

By Fabrizio Montesi. Created on 2023-05-15. Last updated on 2024-12-17.
See also: Introduction to Choreographies

Table of Contents (click to show)

A choreography has the knowledge of choice property if it ensures that, when a choice is made to pick between alternative behaviours, all affected participants are made aware of the choice [Montesi 2023]. The name 'knowledge of choice' was introduced by Castagna et al. [2012] in the context of multiparty session types, but the problem is older and applies to all choreographic languages.

The problem

Consider the following choreography for single sign-on. A client (c) communicates some credentials to an authenticator (a), which then decides if a web service (ws) should communicate a new session token to the client. In the negative case, the web service should communicate a special NoToken value to the client, denoting failure.

c.credentials -> a.x;
if a.valid(x) then
	ws.newToken() -> c.token
else
	ws.NoToken -> c.token

A simplistic choreography for single sign-on, given in the language of Recursive Choreographies. As we are going to see, there is a problem with this choreography.

sequenceDiagram
	participant c
	participant a
	participant ws
	c->>a: credentials
	alt a.valid(credentials)
		ws->>c: newToken()
	else
		ws->>c: NoToken
	end

The same choreography, but given as a sequence diagram.

There is a problem here. The behaviour of ws depends on the internal choice made by a regarding c's credentials. In other words, ws needs to know about a's choice. However, there is no communication that ever reaches ws carrying information about a's choice.

Therefore, this choreography does not ensure knowledge of choice. While there is nothing wrong with this in principle, lack of knowledge of choice can be very relevant in practice. For example, here, the implementor of the choreography will be forced to develop some mechanism by which ws gets to know about a's choice. This can have bad consequences:

The implementor might decide to add extra communications in the implementation, for example the communication of a Boolean from a to ws that would inform ws about a's choice. But this would entail that the choreography would not be representative anymore, since the implementation would enact unforeseen communications.
The implementor might decide to use hidden side-effects that break decentralisation or introduce tight coupling. For example, one could use a shared database to store a's choice (a would write it and ws would read it).

A better solution is to fix the choreography.

Achieving knowledge of choice

Fixing our choreography is relatively simple. We just need to add communications that allow ws to infer what it should do. Here is the resulting choreography, both in textual and visual forms.

c.credentials -> a.x;
if a.valid(x) then
	a -> ws[OK];
	ws.newToken() -> c.token;
else
	a -> ws[KO];
	ws.NoToken -> c.token;

sequenceDiagram
	participant c
	participant a
	participant ws
	c->>a: credentials
	alt a.valid(credentials)
		a->>ws: OK
		ws->>c: newToken()
	else
		a->>ws: KO
		ws->>c: NoToken
	end

The corrected version of the previous choreography, which now ensures knowledge of choice.

Compared to the previous choreography, we have added two selections. A selection is a communication that carries a constant value. In practice, it is usually an instance of an enumerated type. In the then-branch, a communicates the label OK to ws, whereas in the else-branch the communicated label is KO. This means that the implementation of ws can now operate as follows:

Receive a label from a.
If the received label is OK, then send newToken() to c. Otherwise, if the received label is KO, then send NoToken to c.

This behaviour can be easily implemented with a local switch construct at ws (or an equivalent construction in whatever language the implementation of ws is written). In pseudocode:

// Implementation of ws

switch( recv from a ) {
case OK:
	send newToken() to c;
case KO:
	send NoToken to c;
}

The theory of these 'switching behaviours' has an elegant algebraic formulation by means of a join operator, called merging, and the join-semilattice that it induces on a process calculus [Montesi 2023]. The idea of a merging operator was originally introduced in [Carbone et al. 2012].

Amendment

The transformation of a choreography into one that guarantees knowledge of choice is called amendment, or repair. There exist automatic procedures for amendment, for example in [Basu and Bultan 2016; Cruz-Filipe and Montesi 2020; Lanese et al. 2013]. At least one is formalised in the Coq theorem prover [Cruz-Filipe and Montesi 2023].

Additional notes

Some choreographic programming frameworks avoid the problem of knowledge of choice by adding extra communications in implementations, e.g., see [Dalla Preda et al. 2017; Shen et al. 2023]. That is, the code compiled for choreographic conditionals include instructions that broadcast the choice made to all other processes. While this is a suboptimal solution, it is simple and remains predictable, so one could argue that the choreography is still representative in this case (choreographic conditionals in this case should be read as both a local choice and a set of communications).

References

Basu, S., Bultan, T. [2016], 'Automated Choreography Repair', Proceedings of FASE 2016. https://doi.org/10.1007/978-3-662-49665-7_2

Castagna, G., Dezani-Ciancaglini, M. & Padovani, L. [2012], 'On global types and multi-party session', Log. Methods Comput. Sci. 8(1). https://doi.org/10.2168/LMCS-8(1:24)2012

Carbone, M., Honda, K., Yoshida, N. [2012], 'Structured Communication-Centered Programming for Web Services', ACM Trans. Program. Lang. Syst. 34(2): 8:1-8:78. https://doi.org/10.1145/2220365.2220367

Cruz-Filipe, L., Montesi, F., 'Now It Compiles! Certified Automatic Repair of Uncompilable Protocols', Proceedings of ITP 2023. https://doi.org/10.48550/arXiv.2302.14622

Dalla Preda, M., Gabbrielli, M., Giallorenzo, G., Lanese, I., Mauro, J. [2017], 'Dynamic Choreographies: Theory And Implementation', Log. Methods Comput. Sci. 13(2). https://doi.org/10.23638/LMCS-13(2:1)2017

Lanese, I., Montesi, F., Zavattaro, G. [2013], 'Amending Choreographies', Proceedings of WWV 2013. https://doi.org/10.4204/EPTCS.123.5

Montesi, F. [2023], 'Introduction to Choreographies', Cambridge University Press. https://doi.org/10.1017/9781108981491

Shen, G., Kashiwa, S., Kuper, L. [2023], 'HasChor: Functional Choreographic Programming for All (Functional Pearl)', CoRR abs/2303.00924. https://doi.org/10.48550/arXiv.2303.00924