PTO-ARCH-MEMORY-MODEL-ORDERING

1// PTO-UNIT: {"id":"PTO-ARCH-MEMORY-MODEL-ORDERING","surface":"arch","classification":["memory-model","ordering"],"depends_on":["PTO-ARCH-MEMORY-MODEL-ATOMICITY"]}2readonly func MemoryCoherenceBefore(left_index: MemoryEventIndex,3                                    right_index: MemoryEventIndex) => boolean4begin5    let left = _MemoryEvents[[left_index]];6    let right = _MemoryEvents[[right_index]];7    return MemoryEventIsWrite(left) && MemoryEventIsWrite(right) &&8           MemoryEventsShareLocation(left, right) &&9           left.coherence_rank < right.coherence_rank;10end;11
12readonly func MemoryReadsFromBefore(write_index: MemoryEventIndex,13                                    read_index: MemoryEventIndex) => boolean14begin15    let write = _MemoryEvents[[write_index]];16    let read = _MemoryEvents[[read_index]];17    return MemoryEventIsWrite(write) && MemoryEventIsRead(read) &&18           read.read_from == write_index;19end;20
21readonly func MemoryExternalReadsFromBefore(write_index: MemoryEventIndex,22                                            read_index: MemoryEventIndex)23                                            => boolean24begin25    if !MemoryReadsFromBefore(write_index, read_index) then return FALSE; end;26    let write = _MemoryEvents[[write_index]];27    let read = _MemoryEvents[[read_index]];28    return write.kind == MemoryEvent_InitialWrite || write.agent != read.agent;29end;30
31readonly func MemoryFromReadBefore(read_index: MemoryEventIndex,32                                   write_index: MemoryEventIndex) => boolean33begin34    let read = _MemoryEvents[[read_index]];35    // An atomic event contains its read and write sides. Its own write is not a36    // later event in from-read; only a distinct coherence successor is.37    if read_index == write_index || !MemoryEventIsRead(read) then return FALSE; end;38    return MemoryCoherenceBefore(read.read_from, write_index);39end;40
41readonly func MemoryProgramOrderLocationBefore(42    left_index: MemoryEventIndex, right_index: MemoryEventIndex) => boolean43begin44    let left = _MemoryEvents[[left_index]];45    let right = _MemoryEvents[[right_index]];46    return left_index < right_index && left.agent == right.agent &&47           left.kind != MemoryEvent_InitialWrite &&48           right.kind != MemoryEvent_InitialWrite &&49           MemoryEventIsAccess(left) && MemoryEventIsAccess(right) &&50           MemoryEventsShareLocation(left, right);51end;52
53readonly func MemoryFenceOrders(left_index: MemoryEventIndex,54                                right_index: MemoryEventIndex) => boolean55begin56    if left_index + 1 >= right_index then return FALSE; end;57    let left = _MemoryEvents[[left_index]];58    let right = _MemoryEvents[[right_index]];59    for fence_number = left_index + 1 to right_index - 1 do60        let fence_index = fence_number as MemoryEventIndex;61        let fence = _MemoryEvents[[fence_index]];62        if fence.kind == MemoryEvent_Fence && fence.agent == left.agent &&63           fence.agent == right.agent &&64           (MemoryEventClass(left) AND fence.fence_predecessor) != Zeros{4} &&65           (MemoryEventClass(right) AND fence.fence_successor) != Zeros{4} then66            return TRUE;67        end;68    end;69    return FALSE;70end;71
72readonly func MemoryPreservedProgramOrderBefore(73    left_index: MemoryEventIndex, right_index: MemoryEventIndex) => boolean74begin75    let left = _MemoryEvents[[left_index]];76    let right = _MemoryEvents[[right_index]];77    if left_index >= right_index || left.agent != right.agent ||78       left.kind == MemoryEvent_InitialWrite ||79       right.kind == MemoryEvent_InitialWrite ||80       !MemoryEventIsAccess(left) || !MemoryEventIsAccess(right) then81        return FALSE;82    end;83    // PTO-TSO preserves R->M and M->W. W->R to another location is the one84    // relaxed program-order pair unless a matching fence or stronger event85    // ordering restores it. Atomics are full ordering points.86    if MemoryEventIsRead(left) || MemoryEventIsWrite(right) ||87       left.kind == MemoryEvent_Atomic || right.kind == MemoryEvent_Atomic then88        return TRUE;89    end;90    if left.order == MemoryOrder_Acquire ||91       left.order == MemoryOrder_AcquireRelease ||92       right.order == MemoryOrder_Release ||93       right.order == MemoryOrder_AcquireRelease then94        return TRUE;95    end;96    return MemoryFenceOrders(left_index, right_index);97end;98
99readonly func MemoryCandidateExecutionValid() => boolean100begin101    if _MemoryEventCount == 0 then return FALSE; end;102    for event_number = 0 to _MemoryEventCount - 1 do103        let event_index = event_number as MemoryEventIndex;104        let event = _MemoryEvents[[event_index]];105        if MemoryEventIsAccess(event) then106            var initial_count: integer = 0;107            for candidate_number = 0 to _MemoryEventCount - 1 do108                let candidate_index = candidate_number as MemoryEventIndex;109                let candidate = _MemoryEvents[[candidate_index]];110                if candidate.kind == MemoryEvent_InitialWrite &&111                   MemoryEventsShareLocation(event, candidate) then112                    initial_count = initial_count + 1;113                end;114                if candidate_index != event_index &&115                   MemoryEventIsAccess(candidate) &&116                   RangesOverlap(event.address, event.size_bytes,117                       candidate.address, candidate.size_bytes) &&118                   !MemoryEventsShareLocation(event, candidate) then119                    // Mixed-size or partially overlapping candidates require120                    // a byte-level coherence extension and fail closed here.121                    return FALSE;122                end;123            end;124            if initial_count != 1 then return FALSE; end;125        end;126        if event.kind == MemoryEvent_InitialWrite && event.coherence_rank != 0 then127            return FALSE;128        end;129        if MemoryEventIsWrite(event) &&130           event.kind != MemoryEvent_InitialWrite then131            if event.coherence_rank == 0 then return FALSE; end;132            var predecessor_found = FALSE;133            for candidate_number = 0 to _MemoryEventCount - 1 do134                let candidate_index = candidate_number as MemoryEventIndex;135                let candidate = _MemoryEvents[[candidate_index]];136                if candidate_index != event_index &&137                   MemoryEventIsWrite(candidate) &&138                   MemoryEventsShareLocation(event, candidate) then139                    if candidate.coherence_rank == event.coherence_rank then140                        return FALSE;141                    end;142                    if candidate.coherence_rank + 1 == event.coherence_rank then143                        predecessor_found = TRUE;144                    end;145                end;146            end;147            if !predecessor_found then return FALSE; end;148        end;149        if MemoryEventIsRead(event) then150            if event.read_from >= _MemoryEventCount then return FALSE; end;151            let source = _MemoryEvents[[event.read_from]];152            if !MemoryEventIsWrite(source) ||153               !MemoryEventsShareLocation(event, source) ||154               event.read_value != source.write_value then155                return FALSE;156            end;157            if event.kind == MemoryEvent_Atomic &&158               event.write_performed &&159               source.coherence_rank + 1 != event.coherence_rank then160                return FALSE;161            end;162        end;163    end;164    return TRUE;165end;166
167readonly func MemoryRelationAcyclic(uniproc: boolean) => boolean168begin169    if _MemoryEventCount == 0 then return TRUE; end;170    var closure: MemoryRelationMatrix;171    for index = 0 to PTO_MODEL_MEMORY_EVENTS - 1 do172        closure[[index]] = Zeros{PTO_MODEL_MEMORY_EVENTS};173    end;174    for left_number = 0 to _MemoryEventCount - 1 do175        let left = left_number as MemoryEventIndex;176        for right_number = 0 to _MemoryEventCount - 1 do177            let right = right_number as MemoryEventIndex;178            var edge = MemoryCoherenceBefore(left, right) ||179                MemoryFromReadBefore(left, right);180            if uniproc then181                edge = edge || MemoryProgramOrderLocationBefore(left, right) ||182                    MemoryReadsFromBefore(left, right);183            else184                edge = edge || MemoryPreservedProgramOrderBefore(left, right) ||185                    MemoryExternalReadsFromBefore(left, right);186            end;187            if edge then closure[[left]][right] = '1'; end;188        end;189    end;190    for via_number = 0 to _MemoryEventCount - 1 do191        let via = via_number as MemoryEventIndex;192        for source_number = 0 to _MemoryEventCount - 1 do193            let source = source_number as MemoryEventIndex;194            if closure[[source]][via] == '1' then195                closure[[source]] = closure[[source]] OR closure[[via]];196            end;197        end;198    end;199    for event_number = 0 to _MemoryEventCount - 1 do200        let event = event_number as MemoryEventIndex;201        if closure[[event]][event] == '1' then return FALSE; end;202    end;203    return TRUE;204end;205
206readonly func MemoryExecutionAllowedTSO() => boolean207begin208    return MemoryCandidateExecutionValid() &&209           MemoryRelationAcyclic(TRUE) && MemoryRelationAcyclic(FALSE);210end;211