The Two-Buyer Protocol

The two-buyer protocol, a.k.a. the bookstore, is a simple interactive protocol between a bookshop and two buyers. It is a classic example used in concurrency research to illustrate the difficulty of communication scenarios with many parties.

The two-buyer protocol was introduced by Honda, Yoshida and Carbone in the original POPL 2008 paper on multiparty sesion types. It has since appeared in countless papers on session types and choreography.

Description

The following description of the protocol comes from the POPL 2008 paper:

As an example, let us consider a simple refinement of the above Buyer-Seller protocol: consider two buyers, Buyer1 and Buyer2, wish to buy an expensive book from Seller by combining their money. Buyer1 sends the title of the book to Seller, Seller sends to both Buyer1 and Buyer2 its quote, Buyer1 tells Buyer2 howmuch she can pay, and Buyer2 either accepts the quote or receives the quote by notifying Seller.

It is extremely awkward (if logically possible) to decompose this scenario into three binary sessions, between Buyer1 and Seller, between Buyer2 and Seller, and between Buyer1 and Buyer2. Abstracting this protocol as three separate session types also means that our type abstraction loses essential sequencing information in this interaction scenario. For validating this conversation scenario as a whole, therefore, the conversation structure should be represented as a single session.

References

The protocol was first described in a paper at POPL 2008:

Honda, Kohei, Nobuko Yoshida, and Marco Carbone. 2008. ‘Multiparty Asynchronous Session Types’. In Proceedings of the 35th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. Association for Computing Machinery. https://doi.org/10.1145/1328438.1328472. pdf

@inproceedings{honda_2008,
	title = {Multiparty {Asynchronous} {Session} {Types}},
	isbn = {978-1-59593-689-9},
	doi = {10.1145/1328438.1328472},
	booktitle = {Proceedings of the 35th {Annual} {ACM} {SIGPLAN}-{SIGACT} {Symposium} on {Principles} of {Programming} {Languages}},
	publisher = {Association for Computing Machinery},
	author = {Honda, Kohei and Yoshida, Nobuko and Carbone, Marco},
	year = {2008}
}

There is also a journal version of this paper:

Honda, Kohei, Nobuko Yoshida, and Marco Carbone. 2016. ‘Multiparty Asynchronous Session Types’. Journal of the ACM 63 (1): 1–67. https://doi.org/10.1145/2827695. pdf

@article{honda_2016,
	title = {Multiparty {Asynchronous} {Session} {Types}},
	volume = {63},
	doi = {10.1145/2827695},
	number = {1},
	journal = {Journal of the ACM},
	author = {Honda, Kohei and Yoshida, Nobuko and Carbone, Marco},
	year = {2016},
	pages = {1--67}
}