Last active
May 26, 2025 16:26
-
-
Save vilterp/bf020abe8401eef9a3f17f934f3aea00 to your computer and use it in GitHub Desktop.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
import { Context, InvariantViolation, System } from "../context"; | |
const useLock = true; | |
type State = | |
| { type: "MoneyHolder"; onHand: number } | |
| { type: "Lock"; holder: string | null; waiters: string[] }; | |
async function atm(ctx: Context<State, Msg>) { | |
const initialAmount = 0; | |
ctx.setState({ | |
type: "MoneyHolder", | |
onHand: initialAmount, | |
}); | |
const withdrawAmount = 100; | |
const client = new StoreClient("bank", "lock", ctx); | |
const resp = await client.withdraw(withdrawAmount); | |
if (resp === "succeed") { | |
const newAmount = initialAmount + withdrawAmount; | |
ctx.setState({ | |
type: "MoneyHolder", | |
onHand: newAmount, | |
}); | |
} | |
} | |
// === store === | |
type StoreReq = { type: "Get" } | { type: "Put"; value: number }; | |
type StoreResp = { type: "PutResp" } | { type: "GetResp"; value: number }; // TODO: add IDs? or should this be done at a lower level? | |
type StoreMsg = StoreReq | StoreResp; | |
class StoreClient { | |
addr: string; | |
lockClient: LockClient; | |
ctx: Context<State, Msg>; | |
constructor(addr: string, lockAddr: string, ctx: Context<State, Msg>) { | |
this.addr = addr; | |
this.lockClient = new LockClient(lockAddr, ctx); | |
this.ctx = ctx; | |
} | |
async withdraw(amount: number): Promise<"succeed" | "fail"> { | |
if (useLock) { | |
return await this.lockClient.withLock(async () => { | |
return this.doWithdraw(amount); | |
}); | |
} else { | |
return await this.doWithdraw(amount); | |
} | |
} | |
async doWithdraw(amount: number): Promise<"succeed" | "fail"> { | |
const val = await this.get(); | |
if (val < amount) { | |
return "fail"; | |
} | |
const newVal = val - amount; | |
await this.put(newVal); | |
return "succeed"; | |
} | |
async get(): Promise<number> { | |
const resp = (await this.ctx.request(this.addr, { type: "Get" })) | |
.payload as StoreResp; | |
// TODO: assert | |
if (resp.type === "GetResp") { | |
return resp.value; | |
} | |
throw new Error("Get failed"); | |
} | |
async put(value: number): Promise<void> { | |
await this.ctx.request(this.addr, { | |
type: "Put", | |
value, | |
}); | |
} | |
} | |
function bankWithInitialAmt(initialAmount: number) { | |
async function store(ctx: Context<State, Msg>) { | |
let amount = initialAmount; | |
ctx.setState({ type: "MoneyHolder", onHand: initialAmount }); | |
while (true) { | |
const req = await ctx.recv(); | |
if (req.payload.type === "Get") { | |
await ctx.send(req.fromActor, { type: "GetResp", value: amount }); | |
} else if (req.payload.type === "Put") { | |
const value = req.payload.value; | |
amount = value; | |
await ctx.send(req.fromActor, { type: "PutResp" }); | |
ctx.setState({ type: "MoneyHolder", onHand: value }); | |
} | |
} | |
} | |
return store; | |
} | |
// === lock === | |
type LockReq = { type: "Acquire" | "Release" }; | |
type LockResp = { type: "Acquired" | "Released" }; | |
type LockMsg = LockReq | LockResp; | |
class LockClient { | |
addr: string; | |
ctx: Context<{}, Msg>; | |
constructor(addr: string, ctx: Context<{}, Msg>) { | |
this.addr = addr; | |
this.ctx = ctx; | |
} | |
async acquire() { | |
await this.ctx.request(this.addr, { type: "Acquire" }); | |
} | |
async release() { | |
await this.ctx.request(this.addr, { type: "Release" }); | |
} | |
async withLock<T>(f: () => Promise<T>): Promise<T> { | |
await this.acquire(); | |
const resp = await f(); | |
await this.release(); | |
return resp; | |
} | |
} | |
async function lock(ctx: Context<{}, Msg>) { | |
let holder: string | null = null; | |
const waiters: string[] = []; | |
while (true) { | |
ctx.setState({ type: "Lock", holder, waiters: [...waiters] }); | |
const req = await ctx.recv(); | |
if (req.payload.type === "Acquire") { | |
if (holder === null) { | |
holder = req.fromActor; | |
req.reply({ type: "Acquired" }); | |
} else { | |
waiters.push(req.fromActor); | |
} | |
} else if (req.payload.type === "Release") { | |
const next = waiters.shift(); | |
if (next !== undefined) { | |
holder = next; | |
ctx.send(next, { type: "Acquired" }); | |
} else { | |
holder = null; | |
} | |
req.reply({ type: "Released" }); | |
} | |
ctx.setState({ type: "Lock", holder, waiters: [...waiters] }); | |
} | |
} | |
const initialAmount = 150; | |
function checkInvariants(states: { | |
[actorID: string]: State; | |
}): InvariantViolation[] { | |
const violations: InvariantViolation[] = []; | |
// return a violation if the total amount of money on hand is greater than | |
// the initial amount for a given key | |
let total = 0; | |
for (const state of Object.values(states)) { | |
if (state.type !== "MoneyHolder") { | |
continue; | |
} | |
total += state.onHand; | |
} | |
if (total > initialAmount) { | |
violations.push( | |
`Invariant violation: \$${total} in the system total, but initial amount was \$${initialAmount}` | |
); | |
} | |
return violations; | |
} | |
// === system === | |
type Msg = LockMsg | StoreMsg; | |
const BankSystem: System<State, Msg> = { | |
impls: { | |
atm1: atm, | |
atm2: atm, | |
bank: bankWithInitialAmt(initialAmount), | |
lock: lock, | |
}, | |
getMessageLabel(message) { | |
switch (message.type) { | |
case "Put": | |
return `Put(${message.value})`; | |
case "Get": | |
return `Get()`; | |
case "GetResp": | |
return `GetResp(${message.value})`; | |
default: | |
return message.type; | |
} | |
}, | |
getNodeLabel(state) { | |
if (state.type === "Lock") { | |
return state.holder ? state.holder : "none"; | |
} | |
return `\$${state.onHand}`; | |
}, | |
checkInvariants, | |
}; | |
export default BankSystem; |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment