12 KiB
| title |
|---|
| Two-Party Buyer Protocol |
{{ page.title }}
This is an extended two-buyer book-purchase protocol, based loosely on an example given in:
K. Honda, N. Yoshida, and M. Carbone, “Multiparty asynchronous session types,” POPL 2008.
The Scenario
A book-seller responds to requests for book prices when asked. A pair of prospective buyers run through a shopping list. For each book, the first buyer offers to split the cost of the book with the second. If the second has enough money left, it accepts; otherwise, it rejects the offer, and the first buyer tries a different split. If the second buyer agrees to a split, it then negotiates the purchase of the book with the book-seller.
The Protocol
Role: SELLER
When interest in bookQuote($title, _) appears, asserts
bookQuote(title, Maybe Float), false meaning not available,
and otherwise an asking-price.
When interest in order($title, $offer-price, _, _) appears,
asserts order(title, offer-price, false, false) for "no sale",
otherwise order(title, offer-price, PositiveInteger, String), an
accepted sale.
Role: BUYER
Observes bookQuote(title, $price) to learn prices.
Observes order(title, offer-price, $id, $delivery-date) to make orders.
Role: SPLIT-PROPOSER
Observes splitProposal(title, asking-price, contribution, $accepted) to make a split-proposal and learn whether it was
accepted or not.
Role: SPLIT-DISPOSER
When interest in splitProposal($title, $asking-price, $contribution, _) appears, asserts splitProposal(title, askingPrice, contribution, true) to indicate they are willing to
go through with the deal, in which case they then perform the role
of BUYER for title/asking-price, or asserts splitProposal(title, asking-price, contribution, false) to indicate they are unwilling
to go through with the deal.
The Code
Type Declarations
First, we declare assertion types for our protocol.
assertion type bookQuote(title, price);
assertion type order(title, price, id, deliveryDate);
assertion type splitProposal(title, price, contribution, accepted);
Utilities
This routine is under consideration for possible addition to the core library.
function whileRelevantAssert(P) {
spawn {
assert P;
stop on retracted Syndicate.observe(P);
}
}
Implementation: SELLER
function seller() {
spawn {
We give our actor two state variables: a dictionary recording our inventory of books (mapping title to price), and a counter tracking the next order ID to be allocated.
We mark each property (entry) in the books table as a field so
that dependency-tracking on a per-book basis is enabled. As a result,
when a book is sold, any client still interested in its price will
learn that the book is no longer available.
We do not enable dependency-tracking for either the books table
itself or the nextOrderId field: nothing depends on tracking
changes in their values.
this.books = {};
field this.books["The Wind in the Willows"] = 3.95;
field this.books["Catch 22"] = 2.22;
field this.books["Candide"] = 34.95;
this.nextOrderId = 10001483;
Looking up a price yields false if no such book is in our
inventory.
this.priceOf = function (title) {
return (title in this.books) && field this.books[title];
};
The seller responds to interest in bookQuotes by asserting a responsive record, if one exists.
during Syndicate.observe(bookQuote($title, _)) {
assert bookQuote(title, this.priceOf(title));
}
It also responds to order requests.
on asserted
Syndicate.observe(order($title, $offerPrice, _, _)) {
We cannot sell a book we do not have, and we will not sell for less than our asking price.
var askingPrice = this.priceOf(title);
if ((askingPrice === false) || (offerPrice < askingPrice)) {
whileRelevantAssert(
order(title, offerPrice, false, false));
} else {
But if we can sell it, we do so by allocating an order ID and replying to the orderer.
var orderId = this.nextOrderId++;
delete field this.books[title];
whileRelevantAssert(
order(title, offerPrice, orderId, "March 9th"));
}
}
}
}
Implementation: SPLIT-PROPOSER and book-quote-requestor
function buyerA() {
spawn* {
var self = this;
Our actor remembers which books remain on its shopping list, and
tries to buy them one at a time, sharing costs with buyerB.
self.titles = ["Catch 22",
"Encyclopaedia Brittannica",
"Candide",
"The Wind in the Willows"];
JavaScript's callback-oriented blocking means that we express our
loop in almost a tail-recursive style, using helper functions
buyBooks and trySplit.
buyBooks();
function buyBooks() {
if (self.titles.length === 0) {
console.log("A has bought everything they wanted!");
return;
}
var title = self.titles.shift();
First, retrieve a quote for the title, and analyze the result.
react {
stop on asserted bookQuote(title, $price) {
if (price === false) {
console.log("A learns that "+title+" is out-of-stock.");
buyBooks();
} else {
console.log("A learns that the price of "+title+
" is "+price);
Next, repeatedly make split offers to a SPLIT-DISPOSER until either one is accepted, or the contribution from the SPLIT-DISPOSER becomes pointlessly small. We start the process by offering to split the price of the book evenly.
trySplit(title, price, price / 2);
}
}
}
}
function trySplit(title, price, contribution) {
console.log("A makes an offer to split the price of "+title+
" contributing "+contribution);
If we are about to offer to split the price, but the other buyer would contribute less than 10c, then it's not worth bothering; we may as well buy it ourselves. Another version of the program could perform the BUYER role here.
if (contribution > (price - 0.10)) {
console.log("A gives up on "+title+".");
buyBooks();
} else {
Make our proposal, and wait for a response.
react {
stop on asserted
splitProposal(title, price, contribution, true) {
console.log("A learns that the split-proposal for "+
title+" was accepted");
buyBooks();
}
stop on asserted
splitProposal(title, price, contribution, false) {
console.log("A learns that the split-proposal for "+
title+" was rejected");
trySplit(title,
price,
contribution + ((price - contribution) / 2));
}
}
}
}
}
}
Implementation: SPLIT-DISPOSER and BUYER
function buyerB() {
spawn {
This actor maintains a record of the amount of money it has left to spend.
this.funds = 5.00;
It spends its time waiting for a SPLIT-PROPOSER to offer a
splitProposal.
on asserted
Syndicate.observe(splitProposal($title,
$price,
$theirContribution,
_))
{
var myContribution = price - theirContribution;
console.log("B is being asked to contribute "+myContribution+
" toward "+title+" at price "+price);
We may not be able to afford contributing this much.
if (myContribution > this.funds) {
console.log("B hasn't enough funds ("+this.funds+
" remaining)");
whileRelevantAssert(
splitProposal(title, price, theirContribution, false));
} else {
But if we can afford it, update our remaining funds and spawn a small actor to handle the actual purchase now that we have agreed on a split.
var remainingFunds = this.funds - myContribution;
console.log("B accepts the offer, leaving them with "+
remainingFunds+" remaining funds");
this.funds = remainingFunds;
spawn {
While waiting for order confirmation, take the opportunity to signal to our SPLIT-PROPOSER that we accepted their proposal.
assert splitProposal(title,
price,
theirContribution,
true);
When order confirmation arrives, this purchase is completed.
stop on asserted order(title, price, $id, $date) {
console.log("The order for "+title+" has id "+id+
", and will be delivered on "+date);
}
}
}
}
}
}
Starting Configuration
ground dataspace {
seller();
buyerA();
buyerB();
}
A Sample Run
Run the program with ../../bin/syndicatec index.js | node from a
checkout of the Syndicate repository.
A learns that the price of Catch 22 is 2.22
A makes an offer to split the price of Catch 22 contributing 1.11
B is being asked to contribute 1.11 toward Catch 22 at price 2.22
B accepts the offer, leaving them with 3.8899999999999997 remaining funds
A learns that the split-proposal for Catch 22 was accepted
A learns that Encyclopaedia Brittannica is out-of-stock.
The order for Catch 22 has id 10001483, and will be delivered on March 9th
A learns that the price of Candide is 34.95
A makes an offer to split the price of Candide contributing 17.475
B is being asked to contribute 17.475 toward Candide at price 34.95
B hasn't enough funds (3.8899999999999997 remaining)
A learns that the split-proposal for Candide was rejected
A makes an offer to split the price of Candide contributing 26.212500000000002
B is being asked to contribute 8.7375 toward Candide at price 34.95
B hasn't enough funds (3.8899999999999997 remaining)
A learns that the split-proposal for Candide was rejected
A makes an offer to split the price of Candide contributing 30.581250000000004
B is being asked to contribute 4.368749999999999 toward Candide at price 34.95
B hasn't enough funds (3.8899999999999997 remaining)
A learns that the split-proposal for Candide was rejected
A makes an offer to split the price of Candide contributing 32.765625
B is being asked to contribute 2.184375000000003 toward Candide at price 34.95
B accepts the offer, leaving them with 1.7056249999999968 remaining funds
A learns that the split-proposal for Candide was accepted
A learns that the price of The Wind in the Willows is 3.95
A makes an offer to split the price of The Wind in the Willows contributing 1.975
The order for Candide has id 10001484, and will be delivered on March 9th
B is being asked to contribute 1.975 toward The Wind in the Willows at price 3.95
B hasn't enough funds (1.7056249999999968 remaining)
A learns that the split-proposal for The Wind in the Willows was rejected
A makes an offer to split the price of The Wind in the Willows contributing 2.9625000000000004
B is being asked to contribute 0.9874999999999998 toward The Wind in the Willows at price 3.95
B accepts the offer, leaving them with 0.718124999999997 remaining funds
A learns that the split-proposal for The Wind in the Willows was accepted
A has bought everything they wanted!
The order for The Wind in the Willows has id 10001485, and will be delivered on March 9th