-- ProcessorInterface.sak
-- last edited by Suzuki:   10-Aug-81  8:32:23  

CacheProcessor: MONITOR = {

CacheSize: CARDINAL = 400B;
DataSize: CARDINAL = 4;

BusProtocol: TYPE = {Fetch, InvalidateVp, Noop, Store, SFetch, ReadMap, SetMapDirty, WriteMap, WriteMapFlags};

MemoryBusType: TYPE = RECORD[
	body: SELECT OVERLAID * FROM
		Instruction => [Op: BusProtocol, Arg: [0..1777777777B]],
		Data => [Data: Word],
		Map => [Flags: MapFlags, Rp: [0..77777777B]],
		Exception => [ExceptionCode: Word]
		ENDCASE];
CacheIndex: TYPE = [0..CacheSize);
CacheArray: TYPE = ARRAY CacheIndex OF
	RECORD [
		data: RECORD [
			body: SELECT OVERLAID * FROM
				Short => [short: ARRAY [0..DataSize) OF Word],
				Long => [long: ARRAY [0..DataSize/2) OF LONG CARDINAL
				]
				ENDCASE
			],
		vp: VirtualPage,
		b: PageOffset,
		rp: RealPage,
		flags: RECORD[
			vaValid,
			raValid,
			ceDirty,
			shared,
			rpDirty: BOOLEAN]];
MapFlags: TYPE = MACHINE DEPENDENT RECORD [
	reserved: [0..37B],
	protectd, dirty, referenced: BOOLEAN];
Instruction: TYPE = {
	Fetch1, Fetch2, Fetch4, Store1, Store2, Store4, Associate, SetF, GetF};
AddressType: TYPE = RECORD[
	body: SELECT OVERLAID * FROM
		Fetch => [vp: VirtualPage, b: PageOffset, w: WordIndex],
		Store => [data: Word],
		SM => [mf: MapFlags, fill: [0..377B], rp: RealPage],
		SMF => [mf: MapFlags, vp: VirtualPage] 
		ENDCASE ];
Word: TYPE = CARDINAL;
VirtualPage: TYPE = [0..77777777B];
PageOffset: TYPE = [0..77B];
WordIndex: TYPE = [0..3];
RealPage: TYPE = [0..177777B];

ProcessorInterface: DEVICE = {
	IN 
		-- From Processor
		Operation: Instruction, Hold, ReqFromProc: BOOLEAN, Address: AddressType, ProcParity, Tag: BOOLEAN, 
		-- From Memory Bus
		AckFromBus, Shared, MemException: BOOLEAN, MemoryBus: MemoryBusType,
		-- From Slave
		Done, Exception, Start, MapEnd, ValidData: BOOLEAN 
	OUT 
		-- To Processor
		AckToProc: BOOLEAN, Address: AddressType, Data: DataType, 
		CacheException, ProcParity, Tag: BOOLEAN,
		-- To Memory Bus
		ReqToBus, MemHold, Shared: BOOLEAN, MemoryBus: MemoryBusType,
		-- To slave
		Next: BOOLEAN
	GUARDIAN { } -- <Errors when undefined opcode is used in MemoryBus>
	STATE Cache: CacheArray, held: BOOLEAN, entryLoc, victimLoc: CacheIndex
	DATAFLOW
	CONTROL {
		victimLoc ← 0;
		DO { ENABLE ExceptionAbort => CONTINUE;
			WHEN ReqFromProc CHANGE: 
			CacheException ← FALSE;
			SELECT Operation FROM
				Fetch1 => Fetch1Proc[];
				Fetch2 => Fetch2Proc[];
				Fetch4 => Fetch4Proc[];
				Store1 => Store1Proc[];
				Store2 => Store2Proc[];
				Store4 => Store4Proc[];
				Associate => AssociateProc[];
				SetF => SetFProc[];
				GetF => GetFProc[]
			ENDCASE;
			held ← Hold;
			AckToProc ← NOT AckToProc} ENDLOOP;
		}
	};
	
--3) Processor Interface procedures

Fetch1Proc: PROC = {
	OneWordAssign: PROC = {
		Address.data ← Cache[entryLoc].data.short[w]; 
		ReleaseArbiter[entryLoc]};
	FetchProc[OneWordAssign]};

Fetch2Proc: PROC = {
	TwoWordsAssign: PROC = {
		Address.data ← Cache[entryLoc].data.long[w/2];
		ReleaseArbiter[entryLoc]};
	FetchProc[TwoWordsAssign]};

Fetch4Proc: PROC = {
	FourWordsAssign: PROC = {
			Address.data ← Cache[entryLoc].data.long[0]; 
			AckToProc ← NOT AckToProc;
			WHEN ReqFromProc CHANGE: Address.data ← Cache[entryLoc].data.long[1]; 
			ReleaseArbiter[entryLoc]};
	FetchProc[FourWordsAssign]};

FetchProc: PROC[WordsAssign: PROC] = {	
	rp: RealPage;
	rpDirty, success: BOOLEAN;
	[vp: vp, b: b, w: w] ← Address;
	DO
		[success, entryLoc] ← VpBMatch[vp, b]; --This will acquire an arbiter at entryLoc
		IF success THEN GOTO CFinal;
		[success, rp, rpDirty] ← SelectVictimAndVpMatch[vp]; --This will acquire an arbiter at victimLoc
		IF success THEN
			Cache[entryLoc] ← [vp: vp, b: b, rp: rp, flags: [vaValid: TRUE, 
				raValid: FALSE, ceDirty: FALSE, shared: FALSE, rpDirty: rpDirty]]
		ELSE {
			ReleaseArbiter[entryLoc];
			[flags, rp] ← ReadMap[vp];
			IF Vacant[flags] THEN GOTO PageFault;
			AcquireArbiter[entryLoc];
			Cache[entryLoc] ← [vp: vp, b: b, rp: rp, flags: [vaValid: TRUE,
				raValid: FALSE, ceDirty: FALSE, shared: FALSE, rpDirty: flags.dirty]]};
		ReleaseArbiter[entryLoc];
		GetMasterCycle[];
		-- If vp is valid then no map operations occurred in between 
		IF Cache[entryLoc].flags.vaValid THEN GOTO Fetch;
		Abort[];
	REPEAT
		Fetch => {
			MemoryBus ← [Op: Fetch, Arg: rp];
			IF Hold THEN MemHold ← TRUE;
			BeginNewPhase[];
			FetchFromBus[entryLoc];
			WordsAssign[];
			MemHold ← FALSE};
		CFinal => {
			WordsAssign[];
			Noop[]};
		PageFault => {
			Address.exception ← PageFault;
			CacheException ← TRUE;
			Noop[]};
	ENDLOOP};
	
VictimDirty: PROC RETURNS[BOOLEAN] = {
	RETURN[Cache[victimLoc].flags.vaValid AND Cache[victimLoc].flags.raValid AND Cache[victimLoc].flags.ceDirty]};

Vacant: PROC[flags: MapFlags] RETURNS[BOOLEAN] = {
	RETURN[flags.protectd AND flags.dirty AND ~flags.referenced]};

Noop: PROC = {
	IF NOT held OR Hold THEN RETURN;
	GetMasterCycle[];
	MemoryBus ← [Op: Noop, Arg: 0];
	BeginNewPhase[]};

Store1Proc: PROC = {
	OneWordStore: PROC[oldLevel:BOOLEAN] = {
		IF oldLevel=ReqFromProc THEN WHEN ReqFromProc CHANGE: NULL;
		Cache[entryLoc].data.short[w] ← Address.data};
	StoreProc[OneWordStore]};

Store2Proc: PROC = {
	TwoWordsStore: PROC[oldLevel:BOOLEAN] = {
		IF oldLevel=ReqFromProc THEN WHEN ReqFromProc CHANGE: NULL;
		Cache[entryLoc].data.long[w/2] ← Address.data};
	StoreProc[TwoWordsStore]};

Store4Proc: PROC = {
	FourWordsStore: PROC[oldLevel:BOOLEAN] = {
		IF oldLevel=ReqFromProc THEN WHEN ReqFromProc CHANGE: NULL;
		Cache[entryLoc].data.long[0] ← Address.data;
		AckToProc ← NOT AckToProc;
		WHEN ReqFromProc CHANGE: Cache[entryLoc].data.long[1] ← Address.data};
	StoreProc[FourWordsStore]};

StoreProc: PROC[WordsStore: PROC] = {
	rp: RealPage;
	oldLevel, rpDirty, success: BOOLEAN;
	[vp: vp, b: b, w: w] ← Address;
	oldLevel ← ReqFromProc;
	AckToProc ← NOT AckToProc;
	DO
		[success, entryLoc] ← VpBMatch[vp, b];
		IF ~success THEN {
			[success, rp, rpDirty] ← SelectVictimAndVpMatch[vp]; --This will acquire an arbiter at victimLoc
			IF success THEN 
				Cache[entryLoc] ← [vp: vp, b: b, rp: rp, flags: [vaValid: TRUE, 
					raValid: FALSE, ceDirty: FALSE, shared: FALSE, rpDirty: rpDirty]]
			ELSE {
				ReleaseArbiter[entryLoc];
				[flags, rp] ← ReadMap[vp];
				IF Vacant[flags] THEN GOTO PageFault;
				IF flags.protected THEN GOTO WriteProtectFault;
				AcquireArbiter[entryLoc];
				Cache[entryLoc] ← [vp: vp, b: b, rp: rp, flags: [vaValid: TRUE, 
					raValid: FALSE, ceDirty: FALSE, shared: FALSE, rpDirty: flags.dirty]]};
			ReleaseArbiter[entryLoc];
			GetMasterCycle[];	-- Obtains the memory bus
			-- Checks the validity of vp
			IF Cache[entryLoc].flags.vaValid THEN GOTO SFetch;
			Abort[]; LOOP};
		IF ~Cache[entryLoc].flags.rpDirty THEN { 
			ReleaseArbiter[entryLoc];
			GetMasterCycle[];
			IF ~Cache[entryLoc].flags.vaValid THEN {HeldNoop[]; LOOP};
			MemoryBus ← [Op: SetMapDirty, vp: vp];
			IF held THEN MemHold ← TRUE;
			AcquireArbiter[entryLoc]; --AcquireArbiter must come before Next so that
			--vaValid will not be invalidated from the back door
			BeginNewPhase[];
			MemHold ← FALSE};
		IF ~Cache[entryLoc].flags.shared THEN GOTO CacheStore;
		ReleaseArbiter[entryLoc];
		GetMasterCycle[];
		IF Cache[entryLoc].flags.vaValid THEN GOTO Store;
		HeldNoop[];
	REPEAT
		CacheStore => {
			Cache[entryLoc].rpDirty ← Cache[entryLoc].ceDirty ← TRUE;
			WordsStore[oldLevel]};
		Store => {
			WordsStore[oldLevel];
			MemoryBus ← [Op: Store, Arg: vp];
			IF Hold THEN MemHold ← TRUE;
			BeginNewPhase[];
			StoreToBus[];
			MemHold ← FALSE};
		SFetch => SFetch[rp, oldLevel, WordsStore];
		PageFault => {
			Address.exception ← PageFault;
			CacheException ← TRUE;
			Noop[]};
		WriteProtectFault => {
			Address.exception ← WriteProtectFault;
			CacheException ← TRUE;
			Noop[]};
	ENDLOOP;
};			 

HeldNoop: PROC = {
	StartHeldInstruction[Op: Noop, Arg: 0];
	MemHold ← FALSE};

Abort: PROC = {
		Cache[victimLoc].flags.vaValid ← FALSE;
		victimLoc ← (victimLoc - 1) MOD CacheSize;
		-- Send noop
		HeldNoop[]};

AssociateProc: PROC = {
	[vp: vp] ← Address;
	[mf: mf, rp: rp] ← Data;
	-- Invalidate Vp
	GetMasterCycle[];
	MemoryBus ← [Op: SM, Arg: vp];
	IF held THEN MemHold ← TRUE;
	BeginNewPhase[];
	MemoryBus ← [Flag: mf, Rp: rp];
	BeginNewPhase[];
	MemHold ← FALSE};

GetFProc: PROC = {
	[vp: vp] ← Address;
	[mf, rp] ← ReadMap[vp];
	Data ← [mf: mf, rp: rp]};

SetFProc: PROC = {
	[mf: newMf, vp: vp] ← Data;
	GetMasterCycle[];
	MemoryBus ← [Op: SMF, Arg: vp];
	IF held THEN MemHold ← TRUE;
	BeginNewPhase[];
	MemoryBus ← [Flags: newMf];
	BeginNewPhase[];
	Address ← MemoryBus;
	MemHold ← FALSE};

--4) Processor Interface to Bus Interface communication

VictimStore: PROC = {
	Cache[victimLoc].flags.vaValid ← FALSE;
	Cache[victimLoc].flags.raValid ← FALSE;
	ReleaseArbiter[victimLoc];
	GetMasterCycle[];
	StartHeldInstruction[Op: Store, Arg: vp];
	StoreToBus[];
	MemHold ← FALSE;
	AcquireArbiter[victimLoc]};	

SFetch: PROC [rp: RealPage, oldLevel: BOOLEAN, WordsStore: PROC] = {
	MemoryBus ← [Op: SFetch, Arg: rp];
	IF Hold THEN MemHold ← TRUE;
	BeginNewPhase[];
	FetchFromBus[entryLoc];
	WordsStore[oldLevel];
	WHEN Done UP: IF Shared THEN StoreToBus[];
	MemHold ← FALSE};

ReadMap: PROC[vp: VirtualPage] RETURNS [mf: Flags, rp: RealPage] = {
	GetMasterCycle[];
	MemoryBus ← [Op: ReadMap, Arg: vp];
	IF held THEN MemHold ← TRUE;
	BeginNewPhase[];
	WHEN MapEnd UP: MemHold ← FALSE;
	WHEN ValidData UP: {
		MemoryBusSuccess ← TRUE;
		[mf: MapFlags, rp: MapRp] ← MemoryBus;
		BeginNewPhase[];
		RETURN[MapFlags, MapRp]}};

--2) Bus Master procedures

GetMasterCycle: PROC = {
	AcquireBus[];
	WHEN Start UP: NULL};

StartHeldInstruction: PROC[Op: BusProtocol, Arg: [0..1777777777B]] = {
	MemoryBus ← [Op: Op, Arg: Arg];
	IF held THEN MemHold ← TRUE;
	BeginNewPhase[]};

BeginNewPhase: PROC = {
	Next ← TRUE;
	WHEN Done UP: Next ← FALSE;
	IF Exception THEN {Noop[]; CacheException← TRUE; SIGNAL ExceptionAbort}};

FetchFromBus: PROC[loc: CacheIndex] RETURNS[word: Word] = {
	WHEN ValidData UP: Cache[loc].data.long[0] ← MemoryBus.Data;
	BeginNewPhase[];
	WHEN ValidData UP: Cache[loc].data.long[1] ← MemoryBus.Data;
	BeginNewPhase[]};

StoreToBus: PROC = {
	MemoryBus.Data ← Cache[loc].data[0];
	BeginNewPhase[];
	MemoryBus.Data ← Cache[loc].data[1];
	BeginNewPhase[]};

-- Cache operations

SelectVictimAndVpMatch: PROC[vp: VirtualPage] RETURNS[success: BOOLEAN, rp: RealPage, rpDirty: BOOLEAN] = {
	victimLoc ← (victimLoc + 1) MOD CacheSize;
	AcquireArbiter[victimLoc];
	entryLoc ← victimLoc; 
	IF VictimDirty[] THEN VictimStore[];
	[success, rp, rpDirty] ← VpMatch[vp]};

}.