-- File CRSSCode.bravo

-- Last edit by

-- BWL on January 13, 1981

-- MBrown on January 20, 1981 4:14 PM

-- the code is devoid of DIRECTORY statements, but it follows the same rules for IMPORTS as present Mesa. hopefully no confusion will arise from the lack of DIRECTORY statements, since included names are usually fully qualified. the code does not observe the Mesa restriction that declarations must precede executable statements in a block. it uses records of TYPEs instead of the true modelling syntax. I am easily confused by things of the form "Foo : TYPE mumble = <<mumble: DEFS = {mumble: PUBLIC TYPE = ... ".

-- All potentially remote calls in the code are explicit (call System.RemoteCall).

-- To come: implement CreateFile. proper monitor for PageImpl, and better treatment of locks. reduce frequency of "unknown" result (transaction history).

FileSystem: DEFS = BEGIN

-- Client interface to file system. Client calls any machine for CreateTransaction, the same machine for FinishTransaction, and the machine holding page p for AccessPage.

AccessOutcome: TYPE = {OK, absent};

TransOutcome: TYPE = Flags.Outcome; -- {committed, aborted, unknown}

FileID: TYPE = PAINT [System.ID, "FileSystem.FileID"];

-- the client as access to a map from FileID to Machine; maybe the FileID contains a useful hint, but in general the map is more complex (packs move). implementing this map is not part of the file system.

Page: TYPE = PACKED ARRAY [0..System.BytesPerPage) OF BYTE;

PageAction: TYPE = {Read, Write};

PageAddr: TYPE = MACHINE DEPENDENT RECORD [
f: FileID, p: LONG CARDINAL];

Transaction: TYPE = MainSet.StableSet;

CreateTransaction: PROC [] RETURNS [t: Transaction];

CreateFile: PROC[t: Transaction] RETURNS [FileID];

AccessPage: PROC[t: Transaction, a: PageAction, p: PageAddr, data: VAR Page]
RETURNS [AccessOutcome];

FinishTransaction: PROC [t: Transaction, how: Outcome]
RETURNS [result: TransOutcome];

END.--FileSystem

FileSystemPrivate: DEFS = BEGIN

-- Internal file system interface.

Write: PROC [item: IntentionItem];

EnumerateLeaves: PROC [p: Leaves.EnProc, a: ANY ← NULL];

END.--FileSystemPrivate

System: DEFS = BEGIN

-- OS kernel support used by file system.

ID: TYPE = ... ;

Machine: TYPE = ... ;

UniqueID: PROC [] RETURNS [ID];

MachineFromID: PROC [ID] RETURNS [Machine];

ThisMachine: PROC [] RETURNS [Machine];

RemoteCall: PROC [at: Machine, proc: PROC [ANY], args: ANY] RETURNS [results: ANY];

ProcessSave: PROC [];

ProcessReset: PROC [];

END.--System

TransactionImpl: PROGRAM IMPORTS MainSet, Flags, FileSystemInternal EXPORTS FileSystem
= BEGIN

-- This module need not be monitored, since multiple execution is perfectly OK.

CreateTransaction: PUBLIC PROC [] RETURNS [t: Transaction] = {

t ← MainSet.Bless[System.UniqueID[]];

MainSet.Create[t] };

FinishTransaction: PUBLIC PROC [t: Transaction, how: Flags.Outcome]
RETURNS [result: Flags.Outcome] = {

System.ProcessSave[];

-- if we get to here, t will complete (without invoking a timeout mechanism). there is no guarantee that result = how, though.

result ← Complete[t, how];

System.ProcessReset[] };

Complete: PROC [t: Transaction, how: Flags.Outcome] RETURNS [Flags.Outcome] = {

outcome: Flags.Outcome;

SELECT MainSet.SetPhase[t, run] FROM

absent => RETURN[unknown];

run => outcome ← Flags.SetOutcome[t, how]; -- Writes the commit record.

closing => ERROR;

closed => outcome ← Flags.GetOutcome[t]; -- Discovers how the transaction should come out.

ENDCASE;

MainSet.SetPhase[t, closed];

-- This SetPhase enumeration makes all of the leaves "ready", that is, each leaf writes a "closed" record and then forces its log.

NoteReadyEvent[];

-- This proc does nothing: it just marks the ready event. All locks are set before the ready event, and all writes occur after the ready event. This is useful in proving other properties about the algorithm.

IF outcome=commit THEN

-- FOR i: Intention IN t DO WritePage[i] ENDLOOP;

MainSet.Enumerate[t, FileSystemInternal.WritePage];

-- Carries out the intentions (does the page writes). Can also erase the intentions as it goes. Depending on the recovery strategy, this can mean as little as writing a record to the log saying that the write enumeration finished.

MainSet.SetPhase[t, absent];

-- Erases the intentions. Not necessary if the Write enumeration erases the intentions as it goes.

RETURN[outcome] };

-- Note that enumeration to SetPhase[t, closed] is also unnecessary if the client is well-behaved, and Leaf.SetPhase[t, closed] is atomic. The argument for this is more subtle. If the closed enumeration is not done, then the Write enumeration must be sure to close each leaf before enumerating it. If the closed enumeration is not done, then the leaves must be prepared to commit or abort at any time; leaves may not abort unilaterally.

END.--TransactionImpl

Flags: DEFS = BEGIN

-- Commit record storage, called from TransactionImpl.Complete only.

Outcome: type = {committed, aborted, unknown};

SetOutcome: PROC [Transaction, Outcome] RETURNS [Outcome]; -- the call SetOutcome[t, unknown] is illegal.

GetOutcome: PROC [Transaction] RETURNS [Outcome];

END.--Flags

FlagsImpl: MONITOR IMPORTS FlagsSet = BEGIN

-- Note that we could have one flags monitor lock per transaction, but it’s not worth it.

flags: FlagsSet.StableSet = FlagsSet.Create[];

SetOutcome: ENTRY PROC [t: Transaction, o: Flags.Outcome] RETURNS [Flags.Outcome] = {

outcome: Flags.Outcome ← GetOutcomeInternal[t];

IF outcome=unknown THEN { FlagsSet.Insert[flags, [t, o]]; RETURN[o] }

ELSE RETURN[outcome] };

GetOutcome: ENTRY PROC [t: Transaction] RETURNS [Flags.Outcome] = {

RETURN[GetOutcomeInternal[t]] };

GetOutcomeInternal: INTERNAL PROC [t: Transaction] RETURNS [o: Flags.Outcome ← unknown] = {

-- FOR f: FlagItem IN flags DO IF f.t = t THEN o ← f.o ENDLOOP;

NoteFlag: FlagsSet.EnProc = { IF i.t=t THEN o←f.o };

FlagsSet.Enumerate[flags, NoteFlag] };

END.--FlagsImpl

PageImpl: MONITOR IMPORTS MainSet EXPORTS FileSystem, FileSystemPrivate = BEGIN

tryAgain: condition;

-- A realistic strategy about locking is to pass a proc p and a ref u to LockConflict below. LockConflict grants the lock immediately if possible, otherwise makes a "reservation" for a re-request, leaves the lock package, and waits out here. The lock package calls p[u] (with no lock package monitors locked) to notify us that the lock is probably available (no guarantee). The proc p should be very simple, e.g. enter page monitor and then notify tryAgain. It is not fair for a process to request the lock in this way, be denied, and then go away without informing the lock package that it is no longer interested. The lock reservation could be held forever in this case, barring some form of timeout. There are the usual safety problems, in that either one of p or u could become dangling if we aren’t careful.

AccessPage: PUBLIC ENTRY PROC[t: Transaction, a: PageAction, p: PageAddr, data: VAR Page] RETURNS [{OK, absent}] = {

-- Access calls the wide SS monitor to insert the intention. The pattern is much the same as the leaf monitor calling the root. It is easy to see this if you think of each page as a separate leaf.

-- The next line is really redundant, but prevents waiting for the lock when the transaction doesn’t exist.

IF System.RemoteCall[at: System.MachineFromID[t.root],
proc: MainSet.SetPhase, args: ArgsToSetPhase[t, run]] # run THEN RETURN[absent];

item: IntentionItem=( SELECT a FROM read => [read[p]], write => [write[p, data]], ENDCASE );

WHILE LockConflict[t, item]=conflict DO WAIT[tryAgain] ENDLOOP;

-- Monitor prevents lock from being set between this and the Insert. Note that it doesn’t prevent it from being cleared; an interesting example of delicate handling of shared data.

-- The following call to Insert both checks for phase=run and atomically inserts the intention/lock

IF MainSet.Insert[t, item]=absent THEN RETURN[absent];

IF a=read THEN ReadPage[p: p, to: data];

RETURN[OK] };

LockConflictOutcome: TYPE = {conflict, OK};

LockConflict: PROC [t: Transaction, newIntent: IntentionItem] RETURNS [LockConflictOutcome] = {

-- Note that all this is entirely local (i.e., involves narrow SS). It would still work if it were not, but an optimized implementation would be infeasible.

-- FOR l IN leaves DO IF l # t.leaf THEN FOR i IN l DO
IF Conflict[i, newIntent] THEN RETURN[conflict] ENDLOOP ENDLOOP;
RETURN[OK]

result: LockConflictOutcome ← OK;

TestConflictAtLeaf: PROC [i: Leaf.StableSet, l: NULL] = {

InConflict: PROC [i: IntentionItem, l: IntentionItem] = {

IF Conflict[i, [p, act]] THEN result ← conflict };

IF i # t.leaf THEN Leaf.Enumerate[i, InConflict] };

FileSystemPrivate.EnumerateLeaves[TestConflictAtLeaf];

RETURN [result] };

ReadPage: PROC [p: PageAddr, to: VAR Page] = { ... };

WritePage: PUBLIC ENTRY PROC [item: IntentionItem] = { ... };

-- Write is called from Complete -> Root.Enumerate -> Leaf.Enumerate only.

Conflict: PROC [i, j: IntentionItem] RETURNS [BOOLEAN] = { ... };

END.--PageImpl

-- Stable Sets.

-- Here is the main interface for stable sets. It is parameterized by the type of item in the set, and by the type used to name the set. Following are the declarations of the various item types, and then the instantiations of SS for the various kinds of stable set we use.

SS: PROC [item: TYPE, ssName: TYPE] RETURNS [SS: TYPE] = BEGIN RETURN[ SS[

StableSet: TYPE = PAINT [ssName.StableSet, PRINTNAME [Item]];

-- unique name for a stable set. must say "ssName.StableSet" so that an SS can be an ssName.

Item: TYPE = item;

Phase: TYPE = {absent, run, closing --volatile only--, closed};

Bless: PROC [id: System.ID] RETURNS [s: StableSet];

-- given a unique ID, produce a unique name for a stable set.

Create: PROC [s: StableSet ← Bless[System.UniqueID[]]];

-- defaulting of s is used in creating Leaves and FlagsSet (1 instance each) only

Insert: PROC [s: StableSet, i: Item] RETURNS [{OK, notRunning}];

SetPhase: PROC [s: StableSet, p: Phase];

Enumerate: PROC [s: StableSet, p: EnProc, a: ANY←NULL];

EnProc: TYPE = PROC [i: Item, l: ANY] RETURNS [ANY] ]];

END;--SS

IntentionItem: TYPE = RECORD [intention stuff];

Leaf: TYPE = SS[item: IntentionItem, ssName: [StableSet: System.ID]];

Root: TYPE = SS[item: Machine, ssName: [StableSet: System.ID]];

MainSet: TYPE = SS[
item: IntentionItem, ssName: [StableSet: RECORD [root: Root.StableSet, leaf: Leaf.StableSet]]];

-- for a one-machine system we make MainSet be what we call Leaf now, and eliminate Leaf, Root, WideSSRootImpl, and WideSSLeafImpl.

Leaves: TYPE = SS[item: Leaf.StableSet, ssName: [StableSet: System.ID]];

FlagsSet: TYPE = SS[item: Flags.FlagItem, ssName: [StableSet: System.ID]];

WideSSRootImpl: MONITOR LOCKS Image[s.root] USING s: MainSet.StableSet

IMPORTS Leaf, Root, MainSet EXPORTS MainSet = {

OPEN MainSet;

Bless: PUBLIC PROC [id: System.ID] RETURNS [s: MainSet.StableSet] = {

RETURN[ [root: Root.Bless[id], leaf: Leaf.Bless[System.UniqueID[]]] ] };

Create: PUBLIC PROC [s: MainSet.StableSet] = {

Root.Create[s.root] };

SetPhase: PUBLIC ENTRY PROC [s: MainSet.StableSet, to: Phase] RETURNS [Phase] = {

Next: ARRAY Phase OF Phase= [absent: run, run: closed, closing: --illegal-- closing, closed: absent];

-- successor function for root Phase; root Phase is never = closing except while SetPhase is executing, and this does not survive a crash since it is volatile.

phaseOnProcEntry: Phase = Root.GetPhase[s.Root];

IF Next[phaseOnProcEntry] # to THEN RETURN[phaseOnProcEntry];

IF to=closed THEN

Root.SetPhase[s.root, closing];

-- FOR m: Machine IN Root.Elements[s.root] DO
-- RemoteCall[m, Leaf.SetPhase, ArgsForSetPhaseAtLeaf[to]] ENDLOOP;

SetPhaseAtLeaf: Root.EnProc = {[] ← System.RemoteCall[at: i, proc: Leaf.SetPhase, args: l] };

Root.Enumerate[s.root, SetPhaseAtLeaf, ArgsForSetPhaseAtLeaf[to]];

[] ← Root.SetPhase[s.root, to];

RETURN[to] };

Enumerate: PUBLIC PROC [s: MainSet.StableSet, p: EnProc, l: ANY] = {

-- Should be called only when phase=closed

-- FOR m: Machine IN Root.Elements[s.root] DO
FOR i: IntentionItem IN Leaf.Elements[m, s] DO p[i, l] ENDLOOP ENDLOOP;

EnumerateAtLeaf: Root.EnProc = {
[] ← System.RemoteCall[at: i, proc: Leaf.Enumerate, args: Args[s.leaf, p, l]] };

Root.Enumerate[s.root, EnumerateAtLeaf, l] };

END.--WideSSRootImpl

WideSSLeafImpl: MONITOR LOCKS Image[s.leaf] USING s: MainSet.StableSet

IMPORTS Leaf, Root, Leaves EXPORTS MainSet, FileSystemPrivate = {

OPEN MainSet;

leaves: Leaves.StableSet = Leaves.Create[]; -- one of these per machine, listing all the leaves

Insert: PUBLIC ENTRY PROC [s: MainSet.StableSet, i: MainSet.Item] RETURNS [{OK, notRunning}] = {

IF Leaf.Phase[s.leaf]=absent THEN {-- Try to register a leaf, and create it if successful

IF System.RemoteCall[System.MachineFromID[s.root],
Root.Insert, ArgsForRootInsert[s.root, System.ThisMachine[]]]=OK THEN {

Leaves.Insert[leaves, s.leaf]; Leaf.Create[s.leaf] } };

IF Leaf.Phase[s.leaf]#run THEN RETURN[notRunning];

Leaf.Insert[s.leaf, i]; RETURN[OK] };

EnumerateLeaves: PUBLIC ENTRY PROC [p: Leaves.EnProc, a: ANY] = {

Leaves.Enumerate[leaves, p, a] };

END.--WideSSLeafImpl

NarrowSSImpl: PROGRAM IMPORTS SS, NSSImage EXPORTS SS = BEGIN

OPEN SS USING [StableSet, Item, Phase];

-- Note that the narrow SS implementation need not be protected by a monitor, since it is only called from some WideImpl, which is monitored. (Exception: lock enumeration). In any case it could not safely use the same Image mechanism, since the root and leaf IDs are already used for this purpose by the wide SS.

-- The preceding comment does not apply in the single machine case, where there are no WideImpls.

Bless: PUBLIC PROC [i: ID] RETURNS [s: StableSet] = {

RETURN[i] };

Create: PUBLIC PROC [s: StableSet] = {

Log.Write[Create, s];

NSSImage.Register[NEW[VolatileNSS←[s, run, false]]] };

Insert: PUBLIC PROC [s: StableSet, i: Item] = {

... };

GetPhase: PUBLIC PROC [s: StableSet] RETURNS [Phase] = {

RETURN[NSSImage.Find[s].phase] };

SetPhase: PUBLIC PROC [s: StableSet, to: Phase] RETURNS [Phase] = {

image: REF NSSImage.VolatileNSS = NSSImage.Find[s];

Next: ARRAY Phase OF Phase= [absent: run, run: closed, closing: closed, closed: absent];

IF Next[image.phase]=to THEN { Log.Write[SetPhase, s, to]; image.phase←to }

ELSE IF image.phase=run and to=closing THEN --volatile only-- image.phase←closing;

IF image.phase=absent THEN { NSSImage.UnRegister[image]; FREE[image]; RETURN[absent] }

ELSE RETURN[image.phase] };

Enumerate: PUBLIC PROC [s: StableSet, p: EnProc, l: ANY] = {

-- Should be called only when phase=closed. (Exception: lock enumeration).

... };

END.--NarrowSSImpl

NSSImage: DEFS = BEGIN

-- This interface maps a NarrowSSN into the volatile representation of a NSS. It does need a monitor implementation.

VolatileNSS: TYPE = RECORD [name: NarrowSS.StableSet, phase: Phase; closing: BOOLEAN, ...];

Register: PROC [REF VolatileNSS];

UnRegister: PROC [REF VolatileNSS];

Find: PROC [SS.StableSet] RETURNS [REF VolatileNSS]; }

END.--NSSImage

Log: DEFS = BEGIN

Write: PROC [logRecordType, values];

END.--Log