PTO-ARCH-GQM

1// PTO-UNIT: {"id":"PTO-ARCH-GQM","surface":"arch","classification":["programming-model","general-queue-management"],"depends_on":["PTO-ARCH-PROGRAMMING-MODEL-EXECUTION-CONTEXT"]}2// PTO-STATE: {"id":"PTO-STATE-ARCH-GQM","classification":["architecture","general-queue-management"],"scope":"system","owner":"PTO-ARCH-GQM","members":["_GQMQueueValid","_GQMQueueAddress","_GQMQueueCapacity","_GQMQueueCount","_GQMQueueHead","_GQMQueueSuspended","_GQMQueueCorrupt","_GQMQueueEntries","_GQMReleaseEpoch","_LastGQMAcquireEpoch","_GQMEventEpoch","_LastGQMEventAddress"],"depends_on":[]}3
4constant PTO_GQM_MAX_CAPACITY = 1023;5
6// This bound sizes executable verification backing. It is not an7// architectural limit on the number of simultaneously initialized queues.8config PTO_MODEL_GQM_QUEUE_SLOTS : integer {1..16} = 4;9
10type GQMQueueSlot of integer {0..PTO_MODEL_GQM_QUEUE_SLOTS-1};11// The lookup result includes one sentinel value.  Use the configured maximum12// as the static type bound so ASLRef can prove assignments for every allowed13// PTO_MODEL_GQM_QUEUE_SLOTS value.14type GQMQueueLookup of integer {0..16};15type GQMQueueCapacity of integer {0..PTO_GQM_MAX_CAPACITY};16type GQMQueueEntryIndex of integer {0..PTO_GQM_MAX_CAPACITY-1};17
18type GQMQueueEntry of record {19    value: Word,20    release_epoch: integer21};22
23type GQMQueueEntryArray of array [[PTO_GQM_MAX_CAPACITY]] of GQMQueueEntry;24type GQMQueueEntryStore of array [[PTO_MODEL_GQM_QUEUE_SLOTS]]25    of GQMQueueEntryArray;26
27type GQMPopResult of record {28    data: Word,29    result: Word30};31
32var _GQMQueueValid : array [[PTO_MODEL_GQM_QUEUE_SLOTS]] of boolean;33var _GQMQueueAddress : array [[PTO_MODEL_GQM_QUEUE_SLOTS]] of Word;34var _GQMQueueCapacity : array [[PTO_MODEL_GQM_QUEUE_SLOTS]]35    of GQMQueueCapacity;36var _GQMQueueCount : array [[PTO_MODEL_GQM_QUEUE_SLOTS]]37    of GQMQueueCapacity;38var _GQMQueueHead : array [[PTO_MODEL_GQM_QUEUE_SLOTS]]39    of GQMQueueEntryIndex;40var _GQMQueueSuspended : array [[PTO_MODEL_GQM_QUEUE_SLOTS]] of boolean;41var _GQMQueueCorrupt : array [[PTO_MODEL_GQM_QUEUE_SLOTS]] of boolean;42var _GQMQueueEntries : GQMQueueEntryStore;43var _GQMReleaseEpoch : integer;44var _LastGQMAcquireEpoch : integer;45var _GQMEventEpoch : integer;46var _LastGQMEventAddress : Word;47
48pure func GQMResult(primary: integer {0..8191},49                    status: bits(2)) => Word50begin51    var result = Zeros{PTO_XLEN};52    result[12:0] = Zeros{13} + primary;53    result[63:62] = status;54    return result;55end;56
57readonly func FindGQMQueue(address: Word) => GQMQueueLookup58begin59    var selected: GQMQueueLookup =60        PTO_MODEL_GQM_QUEUE_SLOTS as GQMQueueLookup;61    for candidate = 0 to PTO_MODEL_GQM_QUEUE_SLOTS - 1 do62        let slot = candidate as GQMQueueSlot;63        if selected == PTO_MODEL_GQM_QUEUE_SLOTS &&64           _GQMQueueValid[[slot]] &&65           _GQMQueueAddress[[slot]] == address then66            selected = slot as GQMQueueLookup;67        end;68    end;69    return selected;70end;71
72readonly func FindFreeGQMQueue() => GQMQueueLookup73begin74    var selected: GQMQueueLookup =75        PTO_MODEL_GQM_QUEUE_SLOTS as GQMQueueLookup;76    for candidate = 0 to PTO_MODEL_GQM_QUEUE_SLOTS - 1 do77        let slot = candidate as GQMQueueSlot;78        if selected == PTO_MODEL_GQM_QUEUE_SLOTS &&79           !_GQMQueueValid[[slot]] then80            selected = slot as GQMQueueLookup;81        end;82    end;83    return selected;84end;85
86readonly func GQMQueueInitialized(address: Word) => boolean87begin88    return FindGQMQueue(address) != PTO_MODEL_GQM_QUEUE_SLOTS;89end;90
91readonly func GQMQueueRemaining(address: Word) => GQMQueueCapacity92begin93    let found = FindGQMQueue(address);94    if found == PTO_MODEL_GQM_QUEUE_SLOTS then95        return 0;96    end;97    let slot = found as GQMQueueSlot;98    return (_GQMQueueCapacity[[slot]] - _GQMQueueCount[[slot]])99        as GQMQueueCapacity;100end;101
102readonly func GQMQueueSuspended(address: Word) => boolean103begin104    let found = FindGQMQueue(address);105    return if found == PTO_MODEL_GQM_QUEUE_SLOTS then106        FALSE107    else108        _GQMQueueSuspended[[found as GQMQueueSlot]];109end;110
111readonly func GQMQueueHeadValue(address: Word) => Word112begin113    let slot = FindGQMQueue(address) as GQMQueueSlot;114    assert _GQMQueueCount[[slot]] > 0;115    return _GQMQueueEntries[[slot]][[_GQMQueueHead[[slot]]]].value;116end;117
118readonly func GQMQueueHeadReleaseEpoch(address: Word) => integer119begin120    let slot = FindGQMQueue(address) as GQMQueueSlot;121    assert _GQMQueueCount[[slot]] > 0;122    return _GQMQueueEntries[[slot]][[_GQMQueueHead[[slot]]]].release_epoch;123end;124
125func ResetGQMState()126begin127    for candidate = 0 to PTO_MODEL_GQM_QUEUE_SLOTS - 1 do128        let slot = candidate as GQMQueueSlot;129        _GQMQueueValid[[slot]] = FALSE;130        _GQMQueueAddress[[slot]] = Zeros{PTO_XLEN};131        _GQMQueueCapacity[[slot]] = 0;132        _GQMQueueCount[[slot]] = 0;133        _GQMQueueHead[[slot]] = 0;134        _GQMQueueSuspended[[slot]] = FALSE;135        _GQMQueueCorrupt[[slot]] = FALSE;136    end;137    _GQMReleaseEpoch = 0;138    _LastGQMAcquireEpoch = 0;139    _GQMEventEpoch = 0;140    _LastGQMEventAddress = Zeros{PTO_XLEN};141end;142
143func InitializeGQMQueue(address: Word,144                        capacity: GQMQueueCapacity) => GQMQueueSlot145begin146    var found = FindGQMQueue(address);147    if found == PTO_MODEL_GQM_QUEUE_SLOTS then148        found = FindFreeGQMQueue();149    end;150
151    // The executable profile must provide enough backing for its workload.152    // This assertion does not define an architectural queue-count limit.153    assert found != PTO_MODEL_GQM_QUEUE_SLOTS;154    let slot = found as GQMQueueSlot;155    _GQMQueueValid[[slot]] = TRUE;156    _GQMQueueAddress[[slot]] = address;157    _GQMQueueCapacity[[slot]] = capacity;158    _GQMQueueCount[[slot]] = 0;159    _GQMQueueHead[[slot]] = 0;160    _GQMQueueSuspended[[slot]] = FALSE;161    _GQMQueueCorrupt[[slot]] = FALSE;162    return slot;163end;164
165func SetGQMQueueSuspended(address: Word, suspended: boolean)166begin167    let found = FindGQMQueue(address);168    if found != PTO_MODEL_GQM_QUEUE_SLOTS then169        _GQMQueueSuspended[[found as GQMQueueSlot]] = suspended;170    end;171end;172
173func SetGQMQueueCorrupt(address: Word, corrupt: boolean)174begin175    let found = FindGQMQueue(address);176    if found != PTO_MODEL_GQM_QUEUE_SLOTS then177        _GQMQueueCorrupt[[found as GQMQueueSlot]] = corrupt;178    end;179end;180
181func BroadcastGQMEvent(address: Word)182begin183    _GQMEventEpoch = _GQMEventEpoch + 1;184    _LastGQMEventAddress = address;185end;186
187func PushGQMQueueEntry(address: Word,188                       value: Word,189                       at_head: boolean,190                       relaxed: boolean,191                       notify_event: boolean) => Word192begin193    let found = FindGQMQueue(address);194    if found == PTO_MODEL_GQM_QUEUE_SLOTS then195        return GQMResult(0, '10');196    end;197
198    let slot = found as GQMQueueSlot;199    if _GQMQueueCorrupt[[slot]] then200        return GQMResult(0, '10');201    end;202
203    let remaining = GQMQueueRemaining(address);204    if _GQMQueueSuspended[[slot]] || remaining == 0 then205        return GQMResult(remaining, '01');206    end;207
208    var entry_index: GQMQueueEntryIndex = 0;209    if at_head then210        if _GQMQueueHead[[slot]] == 0 then211            entry_index = (_GQMQueueCapacity[[slot]] - 1)212                as GQMQueueEntryIndex;213        else214            entry_index = (_GQMQueueHead[[slot]] - 1)215                as GQMQueueEntryIndex;216        end;217        _GQMQueueHead[[slot]] = entry_index;218    else219        entry_index = ((_GQMQueueHead[[slot]] + _GQMQueueCount[[slot]])220            MOD _GQMQueueCapacity[[slot]]) as GQMQueueEntryIndex;221    end;222
223    var release_epoch: integer = 0;224    if !relaxed then225        _GQMReleaseEpoch = _GQMReleaseEpoch + 1;226        release_epoch = _GQMReleaseEpoch;227    end;228    _GQMQueueEntries[[slot]][[entry_index]].value = value;229    _GQMQueueEntries[[slot]][[entry_index]].release_epoch = release_epoch;230    _GQMQueueCount[[slot]] = (_GQMQueueCount[[slot]] + 1)231        as GQMQueueCapacity;232
233    if notify_event then234        BroadcastGQMEvent(address);235    end;236    return GQMResult(GQMQueueRemaining(address), '00');237end;238
239func PopGQMQueueEntry(address: Word,240                      relaxed: boolean,241                      notify_event: boolean) => GQMPopResult242begin243    var response = GQMPopResult {244        data = Zeros{PTO_XLEN},245        result = GQMResult(0, '10')246    };247    let found = FindGQMQueue(address);248    if found == PTO_MODEL_GQM_QUEUE_SLOTS then249        return response;250    end;251
252    let slot = found as GQMQueueSlot;253    if _GQMQueueCorrupt[[slot]] then254        return response;255    elsif _GQMQueueCount[[slot]] == 0 then256        response.result = GQMResult(0, '01');257        return response;258    end;259
260    let head = _GQMQueueHead[[slot]];261    let entry = _GQMQueueEntries[[slot]][[head]];262    let next_head = ((head + 1) MOD _GQMQueueCapacity[[slot]])263        as GQMQueueEntryIndex;264    _GQMQueueHead[[slot]] = next_head;265    _GQMQueueCount[[slot]] = (_GQMQueueCount[[slot]] - 1)266        as GQMQueueCapacity;267    if _GQMQueueCount[[slot]] == 0 then268        _GQMQueueHead[[slot]] = 0;269    end;270
271    if !relaxed && entry.release_epoch != 0 then272        _LastGQMAcquireEpoch = entry.release_epoch;273    end;274    if notify_event then275        BroadcastGQMEvent(address);276    end;277    response.data = entry.value;278    response.result = GQMResult(_GQMQueueCount[[slot]], '00');279    return response;280end;281