/*The bulk of this model is a simple abstract representation of a cache. However, in my predicate directMapVersusTwoWay, I lay constraints to force the analyzer to compare a direct cache against a two way cache, and find a sequence of instructions that cause the direct mapped cache to out perform the two way cache.
*/

/*A line in actual memory*/
sig Line{}

/*A line in the cache*/
sig CacheLine{}

/*A set of lines in the cache*/
sig CacheSet{}

abstract sig HitStatus{}

one sig Hit, Miss extends HitStatus{}

/*The state of the cache at a certain time. Incorporates the next memory line to be accessed.
Also includs a hit status i.e. whether executing this State caused a hit or a miss. Note on the
last State: The last State has no hitStatus as it is not considered as part of the execution.
Although it has a nextLine field, this is ignored and this last State is to be considered as
the State where the execution stops i.e. it is NOT part of the execution. */
sig State{
hitStatus : lone HitStatus, //Whether nextLine caused a hit in the next State ro a miss
lineMap : CacheLine lone -> lone Line, //A map of what line (if any) in memory is mapped to each cahe line
nextLine : one Line //The next Line in memory to be accessed. This will be in the cache in the next State.
}

/*An execution from the point of view of the cache i.e. a sequence of memory accesses and
the state of the cache at each access. Note: The last State in the execution is the terminating
State and is not considered to be part of this execution.*/
sig Execution{
numMisses : one Int, //The number of cache misses during this execution
associatedLines : CacheSet lone -> set Line, //Maps each CacheSet to a set of lines in memory
associatedCacheLines : CacheSet one -> set CacheLine, //Maps each CacheSet to a set of CacheLines
states : seq State
}{
let S = states.elems{
//All states in this execution
all s : S{
//The lineMap relations of states in this execution only maps lines to cacheLines in
//the associated set, which is given in the associatedLines relation of this execution.
all cL : CacheLine | some cL.(s.lineMap) => cL.~associatedCacheLines = cL.(s.lineMap).~associatedLines
}
}

//Set of all indices of the sequence of states whose elements' statuses were misses
let missSet = {i : Int | (states[i]).hitStatus = Miss}
{
#missSet = numMisses
}
}

//Every State is in some execution (Not really a necessary constraint but gets rid of useless states)
fact allStatesinExecutions
{
Execution.states.elems = State
}

//All cache sets have the same number of lines and cache lines associated with them, within an executinon.
fact equalSetSize{
all e : Execution, c, c' : CacheSet{
//If both sets have lines associated with them, constrain them having equal lines and cache lines
(c.(e.associatedLines) != none and c'.(e.associatedLines) != none) =>
{
#c.(e.associatedLines) = #c'.(e.associatedLines) //All sets have same number of lines associated with them
#c.(e.associatedCacheLines) = #c'.(e.associatedCacheLines) //All sets have same number of cacheLines associated with them
}
//A set must either contain both lines and cache lines or nothing at all
(c.(e.associatedLines) = none) <=> (c.(e.associatedCacheLines) = none)
(c'.(e.associatedLines) = none) <=> (c'.(e.associatedCacheLines) = none)
}
}

//No lines or cache lines are floating around not in a set.
fact allLinesInSets{
all e : Execution | CacheSet.(e.associatedLines) = Line and CacheSet.(e.associatedCacheLines) = CacheLine
}

//Cache begins empty in every execution
//First State's hit status is null
fact initCache{
all e : Execution{
no e.states[0].lineMap //No cache lines are mapped to real lines
no (e.states.last).hitStatus //Can't have a status as execution stops here.
}
}

//s is the previous State and s' the next State. s' contains the nextLine of s in its cache.
//This predicate models the transition between one state and the next. Here, s' is the resulting
//State when nextLine of s is accessed.
pred addLine[s, s' : State, e : Execution]{
let map = s.lineMap, map' = s'.lineMap, next_line = s.nextLine, next_set = next_line.~(e.associatedLines){
let cache_lines = next_set.(e.associatedCacheLines), free = cache_lines - map.Line{
(some map.next_line) =>
{
(map' = map) //If the next line is in cache, then don't change it.
s.hitStatus = Hit //If the line was in cache, we have a cache hit.
}
(no map.next_line) =>
{
one c : cache_lines | map' = map ++ c -> next_line //Else map one cache line to next line
(some free) => one c : free | map' = map + c -> next_line //If there is some free cache line in the set corresponding to next_line, use it
s.hitStatus = Miss //if the line had to be replaces, we have a cache miss.
}
}
}
}

fact validTransitions{
all e : Execution, i : Int{
let S = e.states{
(some S[i] and some S[i+1]) => addLine[S[i], S[i + 1], e]
}
}
}

pred differentSetSize{
all e, e' : Execution{
(e != e') => #(e.associatedLines).Line != #(e'.associatedLines).Line
}
}

pred test{
differentSetSize
#CacheSet > 2
#CacheLine < #Line
#CacheLine > 2
#State > 7
}

//Tries to find an execution that would cause a direct mapped Cache to out perform a
//two way associative cache
pred directMapVersusTwoWay{
#Execution = 2
some e, e' : Execution, c, c' : CacheSet{
(e != e')
#c.(e.associatedCacheLines) = 2 //e is the two way
#c'.(e'.associatedCacheLines) = 1 //e' is the direct mapped

//The two execution share the same number of states and the same memory accesses
all i : Int{
e'.states[i].nextLine = e.states[i].nextLine
}

e.numMisses > e'.numMisses //More misses in the 2 way execution than the direct mapped one
}
}

//During a particular execution, no two cache set share either cache lines or lines
assert noLineOverlap{
all e : Execution, cS, cS' : CacheSet | (cS != cS') =>
{
no (cS.(e.associatedLines) & cS'.(e.associatedLines))
no (cS.(e.associatedCacheLines) & cS'.(e.associatedCacheLines))
}
}

check noLineOverlap for 10

run test for 6 but 6 int, exactly 2 Execution

run directMapVersusTwoWay for 7