About a week ago, while looking into papers, I diagonally stumbled into a concept of choreographic programming. The idea is that instead of writing a separate program for each endpoint, we could simultaneously write a single program for all participants in a simple Alice and Bob notation, as one can find in protocol descriptions on Wikipedia. The hard part, though, is designing reasonably clear primitives while being able to project them to endpoints correctly, and this is what the vast research on choreographic programming is about.
The most minimal taste of choreographic programming is describing the types/labels of messages which travel between participants while leaving the implementation of the endpoints to a programmer. The benefit of doing so is that implementers of the protocol are free to choose their language and use the global specification to test that it is correct, just like typing does in statically typed programming languages. It is, in fact, called multiparty session types, where session refers to communication which takes place.
A recent example gaining popularity in this direction is Scribble. A typical code for it is shown below:
global protocol BookJourney (role Customer as C, role Agency as A, role Service as S) {
rec LOOP {
choice at C {
query (journey: String) from C to A;
price (Int) from A to C:
info (String) from A to S;
continue LOOP;
} or {
choice at C {
ACCEPT() from C to A;
ACCEPT() from A to S;
Address(String) from C to S;
(Date) from S to C;
} or {
REJECT() from C to A;
REJECT() from A to S;
} } } }
Chor takes another approach. In addition to defining communication types, it also allows for writing the protocol in one block for all endpoints at the same time:
program customer_agency;
protocol PurchaseProtocol {
Customer -> Agency: CheckPrice
askPrice(string);
}
protocol CheckPrice {
Agency -> Customer: price(int);
Customer -> Agency: {
askPrice(string);
CheckPrice,
accept(void);
Customer -> Agency: order(string);
Agency -> Customer: date(string),
reject(void)
}
}
public agency_url: PurchaseProtocol
define checkPrice(c,a)(s[CheckPrice:c[Customer], a[Agency]]) {
ask@a(prod,price);
a.price -> c.price: price(s);
ask@c(price,satisfied);
if(satisfied == "Yes")@c {
ask@c("Confirm?",confirm);
if (confirm == "Yes")@c {
c -> a: accept(s);
c.prod -> a.prod: order(s);
ask@a(prod,date);
a.date -> c.date: date(s)
} else {
c-> a: reject(s)
}
} else {
ask@c("Product Name",prod);
c.prod -> a.prod: askPrice(s);
checkPrice(c,a)(s)
}
}
main {
c[Customer] start a[Agency]: agency_url(s);
ask@c("Product Name",prod);
c.prod -> a.prod: askPrice(s);
checkPrice(c,a)(s)
}
Notice the @; it is a way of telling that the function is executed on a particular endpoint. Although It is a bit ugly that new variables are created within the functions.
A Pirouette uses an alternative approach, where a multiparty session type is constructed from the program itself.
Buyer.book_title ⇝ Seller.b;
Seller.prices[b] ⇝ Buyer.p;
if Buyer.(b < budget)
then Buyer[L] ⇝ Seller;
Seller.get_delivery_date(b) ⇝ Buyer.d_date;
Buyer.(Some d_date)
else
Buyer[R] ⇝ Seller;
Buyer.None
And it also attempts to describe what functions of a global protocol could look like. Unfortunately, currently, this language does not seem to be implemented.
Academically choreographic programming language can be used as an approachable alternative to describing a protocol to prove its security properties. The best one that struck me in investigating the choreographic programming landscape is available in the paper "Security Protocols as Choreographies":
Alice → TPM: Boot
TPM:pcr:=’1’
TPM → Alice: Booted
Alice: new n, new esk
Alice → TPM: Session , tpmk , aenc(esk , tpmk)
TPM: new sid
TPM → Alice:sid
Alice → TPM:senc((Extend , n, sid), esk)
TPM: pcr := hash(n, pcr)
TPM → Alice: Extended
Alice → TPM: Create , hash(’obt ’, pcr)
TPM:newk
TPM → Alice:sign((Created ,k,hash(’obt ’, pcr)), inv(tpmk) )
Alice:new v
Alice → Parent: Envelope , enc(v, k)
Parent: new esk
Parent → TPM: Session , aenc(esk, tpmk)
TPM: new sid
TPM → Parent:sid
Parent → TPM:{
senc((Extend ,’ref ’, sid), esk):
TPM: pcr := hash(’ref ’, pcr)
TPM → Parent: Extended
Parent → TPM: Quote ,enc(v,k)
TPM → Parent:sign((Quoted ,pcr,enc(v,k)),inv(tpmk))
event secret(v)
+
senc((Extend ,’obt ’, sid), esk):
TPM: pcr := hash(’obt ’, pcr)
TPM → Parent: Extended
Parent → TPM: Decrypt , enc(v, k), sign((Created , k, pcr), inv ( tpmk ))
TPM → Parent:v
}
Apart from the fact that it does not use variables, it is a language I would love to program distributed systems.
Imagining a choreographic DSL in Julia
The most attractive approach, in my opinion, is taken by Piriotette. However, branching does feel a bit sloppy, where the programmer is expected to inform relevant endpoints on which branch is taken after the branch is taken. Also, the dot syntax is so OOP and ; is perhaps unnecessary, as we can see in the previous code example. Let's see if that can be made syntactically better.
The sending of messages could follow a simple Alice and Bob notation using a column as it is often done and presume that variable names at endpoints do have the same name and provide the as keyword to set it different at the endpoint.
Buyer -> Seller: book_title
Seller -> Buyer: prices[book_title] as p
So that was simple. Let's now jump into branching. It would be great that the branching part of the code would not involve informing involved parties on which branch has been taken. This is why I find this syntax most appropriate:
Buyer: choice = price < budget ? Left : Right
select Buyer -> Seller [choice]
case Left:
# WHAT TO DO IN THIS BRANCH
case Right:
# WHAT TO DO IN THIS BRANCH
end
Which follows the TPM example and replaces {} with case <label>:, adds a select keyword for signifying what it is. A bracket is added for informing how choice is calculated [<choice>] and follows the academic convention as a->b[l] is used to denote a label in process calculus (read it somewhere).
The last thing we must consider is how this protocol shall be packaged and used. Each agent can have its own set of inputs in the protocol. That we can address by having a function signature like:
function BookSeller((book_title, budget)@Buyer, (get_delivery_date)@Seller)
...
Buyer: return "Finished."
Seller: return "Done."
end
Note that the use of @ may not sit well within Julia, which uses it for calling macros. Any other symbol may suffice there.
The primary motivation for writing the protocol in a single function is that we want to test that it works. In contrast to the usual situation where one needs to call the code concurrently at the endpoints and deal with errors being hidden in those threads, an alternative way could be simply running it run globally:
book_title = "Iliad"
budget = 100
get_deliver_date(x) = 2050
result = BookSeller((book_title, budget)@Buyer, (get_delivery_date)@Seller)
@test result@Buyer == "Finished."
@test result@Seller == "Done."
We take the BookSeller protocol and project it with corresponding endpoints to run the protocol at the endpoints.
io = Link()
t1 = @async begin
book_title = "Iliad"
budget = 100
BookSeller@Buyer(book_tile, budget; Seller=io)
end
t2 = @async begin
get_deliver_date() = 2050
BookSeller@Seller(get_delivery_date; Buyer=io)
end
@test result(t1) == "Finished."
@test result(t2) == "Done."
To implement Link, only send and recv functions need to be supplemented:
send(x::Int, io::Link) = raw_send(string(x), io)
recv(::Type{Int}, io::Link) = parse(Int, raw_recv(io))
This way, we can reuse the same protocol with different serialisation formats of choice, let it be either "JSON", "TOML", or even "ASN.1".
To assist in implementing a data marshalling channel, it would be helpful to infer the types of messages used for communication and test the link implementation accordingly. At the high level, it could look something like:
message_types = infer_message_types(BookSeller, ((String, Int)@Buyer, (typeof(get_delivery_date)@Seller))
@test isspecified(Link, message_types)
The isspecified method would then go through each message type and check that the corresponding method for marshalling and unmarshalling is implemented. In addition, if the type implements a sample method returning some random value for a given type, it could also check statistically that unmarshal(marshal(x))==x.
Lastly, a monitor could be fired up at the endpoint. That way, it could be detected if a remote party deviates from the protocol. However, this would require every message to have a unique distinct label for unmarshaling without input from the protocol.
Lastly, to finish this speculative specification, let's discuss modularity. Functions are integral to any large-scale program, allowing us to test things in pieces and assemble complex protocols. Taking inspiration from Pirouette, I arrive at the following idea:
function BookSeller(F, (book_title, budget)@Buyer, (get_delivery_date)@Seller)
Buyer -> Seller: book_title
Buyer: decision = F((prices[b])@Seller, (budget)@Buyer))
select Buyer -> Seller [decission]
case Left:
Seller -> Buyer: get_delivery_date(book_title) as d_date; # We expect no output from the Seller
Buyer: return d_date
case Right:
Buyer: return nothing
end
end
The function then could be as simple as:
function F((p)@Seller, (budget)@Buyer)
Seller -> Buyer: p
Buyer: return p < budget
end
To pass it to the BookSeller, we could do something as simple as:
result = BookSeller(F, (book_title, budget)@Buyer, (get_delivery_date)@Seller)
Similarly, we could proceed at the endpoint.
A difficulty arises when we want to introduce another agent within the protocol. Consider another implementation of F:
function F((p)@Seller, (budget)@Buyer, ()Buyer2)
Seller -> Buyer, Buyer2: p
Buyer2 -> Buyer: p/2 as contrib
Buyer: return (p - contrib) < budget
end
To test it, we could proceed using a closure:
G((p)@Seller, (budget)@Buyer) = F((p)@Seller, (budget)@Buyer, ()@Buyer2)
result = BookSeller(G, (book_title, budget)@Buyer, (get_delivery_date)@Seller)
A bit ugly part is that G needs to be provided with a link for Buyer2 explicitly, which needs to be done with closure or redefinition of the protocol:
BookSellerExtended((p)@Seller, (budget)@Buyer, ()@Buyer2) = BookSeller(
((p)@Seller, (budget)@Buyer) -> F((p)@Seller, (budget)@Buyer, ()@Buyer2),
(book_title, budget)@Buyer, (get_delivery_date)@Seller
)
Whether it is defined here or at the endpoint is a matter of taste. In some situations where a complete F is unavailable, it could be implemented at the endpoint and placed in a place of F though that no longer could provide guiding rails to assist correct implementation.
It was fun to think about this problem, but it seems like an overwhelming project to take on. The main question remains whether it would be usable in practice and whether, if such DSL existed for what kind of problems it would be best suited for. Dining philosophers do not seem to be one of them, whereas a symmetric block cypher seems plausible if recursion or jumps are used at select statements.
Anyway, my itch with investigating and writing this post is scratched. I hope you enjoy thinking about choreographic programming, what it could enable you to do, and its pitfalls.
References
- Bruni, A., Carbone, M., Giustolisi, R., Mödersheim, S., Schürmann, C. Security Protocols as Choreographies. (2021)
- S. Giallorenzo, F. Montesi, M. Peressotti, D. Richter, G. Salvaneschi, and P. Weisenburger, Multiparty Languages: The Choreographic and Multitier Cases. (2021)
- D. Ancona et al., Behavioral Types in Programming Languages, FNT in Programming Languages. (2016)
- Andrew K. Hirsch and Deepak Garg. Pirouette: Higher-Order Typed Functional Choreographies https://www.youtube.com/watch?v=ES1bhxcRDy0 (2022)
- Cover image: https://pxhere.com/en/photo/1606406
Top comments (0)