PTO-SCALAR-MODEL-AMO-SEMANTICS

1// PTO-UNIT: {"id":"PTO-SCALAR-MODEL-AMO-SEMANTICS","surface":"scalar","classification":["model","amo","semantics"],"depends_on":["PTO-SCALAR-MODEL-AGU-ADDRESSING","PTO-ARCH-MEMORY-MODEL-ATOMICITY"]}2// PTO-REQ-SCALAR-AMO-001, PTO-REQ-MEMORY-TSO-001: LR/SC, CAS, and atomic3// read-modify-write operations represented as indivisible TSO events.4
5readonly impdef func AtomicAddress(address: Word, far: boolean) => Word6begin7    // The portable model has one flat address domain. FAR remains an explicit8    // address-class hint so profiles can refine it without changing decoding.9    if far then return address; else return address; end;10end;11
12pure func NormalizeAtomicReturn(value: Word,13                                size_bytes: integer {1,2,4,8}) => Word14begin15    case size_bytes of16        when 1 => return ZeroExtend{PTO_XLEN}(value[7:0]);17        when 2 => return ZeroExtend{PTO_XLEN}(value[15:0]);18        when 4 => return SignExtend{PTO_XLEN}(value[31:0]);19        when 8 => return value;20    end;21end;22
23// DMA copies one 64-byte command payload. Both ranges are translated and24// permission-checked before any byte is read or written. Source bytes are25// snapshotted before the destination commit, so overlapping ranges have26// memmove semantics and any fault leaves memory unchanged.27func ExecuteScalarDMACopy64(source_address: Word, destination_address: Word)28begin29    let source_probe = ProbeDataAccess(source_address, 64, 1, FALSE);30    if RaiseDataAccessFault(source_probe, source_address) then31        return;32    end;33
34    let destination_probe = ProbeDataAccess(destination_address, 64, 1, TRUE);35    if RaiseDataAccessFault(destination_probe, destination_address) then36        return;37    end;38
39    let snapshot = LoadTranslatedBytes64(source_probe.translated_address);40    var event_values: array [[8]] of Word;41    for chunk = 0 to 7 do42        let offset = (chunk * 8) as integer {0..262144};43        let translated_source = source_probe.translated_address +44            NaturalToWord(offset);45        let snapshot_value = Bytes64ChunkValue(snapshot, chunk);46        event_values[[chunk]] = snapshot_value;47        RecordLoadEvent(48            translated_source,49            8,50            snapshot_value,51            MemoryOrder_Relaxed);52    end;53
54    StoreTranslatedBytes64(55        destination_address,56        destination_probe.translated_address,57        snapshot);58
59    for chunk = 0 to 7 do60        let offset = (chunk * 8) as integer {0..262144};61        let translated_destination = destination_probe.translated_address +62            NaturalToWord(offset);63        RecordStoreEvent(64            translated_destination,65            8,66            event_values[[chunk]],67            MemoryOrder_Relaxed);68    end;69end;70
71func LoadReserved(address: Word, size_bytes: integer {1,2,4,8},72                  order: MemoryOrder) => Word73begin74    let result = LoadWithOrder(address, size_bytes, order);75    // A fault has no LR reservation effect. In particular, it preserves an76    // older reservation rather than replacing or clearing it.77    if _LastFault == Fault_None then78        _ReservationValid = TRUE;79        _ReservationAddress = address;80        _ReservationSize = size_bytes;81    end;82    return result;83end;84
85func StoreConditional(address: Word, size_bytes: integer {1,2,4,8},86                      value: Word, order: MemoryOrder) => Word87begin88    let reservation_granule = ReservationGranuleAddress();89    let requested_granule = address - NaturalToWord(90        (UInt(address) MOD PTO_RESERVATION_GRANULE_BYTES) as91            integer {0..262144});92    // PTO's local exclusive monitor is cache-line based: SC width and exact93    // byte address do not narrow the reservation once the 64-byte line matches.94    let succeeds = _ReservationValid && reservation_granule == requested_granule;95    if succeeds then96        // Every SC attempt clears the local monitor, including a successful97        // reservation check followed by an access fault.98        _ReservationValid = FALSE;99        let probe = ProbeDataAccess(address, size_bytes, size_bytes, TRUE);100        if RaiseDataAccessFault(probe, address) then return Zeros{PTO_XLEN}; end;101        StoreTranslated(address, probe.translated_address, size_bytes, value);102        RecordStoreEvent(probe.translated_address, size_bytes, value, order);103        return Zeros{PTO_XLEN};104    else105        // A reservation miss is deliberately probe-free, even when address is106        // misaligned or outside the active access domain.107        _ReservationValid = FALSE;108        return Zeros{PTO_XLEN} + 1;109    end;110end;111
112pure func AtomicValue(op: AtomicOperation, old_value: Word, operand: Word) => Word113begin114    case op of115        when Atomic_SWAP => return operand;116        when Atomic_ADD  => return old_value + operand;117        when Atomic_AND  => return old_value AND operand;118        when Atomic_OR   => return old_value OR operand;119        when Atomic_XOR  => return old_value XOR operand;120        when Atomic_SMIN =>121            if SInt(old_value) < SInt(operand) then return old_value; else return operand; end;122        when Atomic_SMAX =>123            if SInt(old_value) > SInt(operand) then return old_value; else return operand; end;124        when Atomic_UMIN =>125            if UInt(old_value) < UInt(operand) then return old_value; else return operand; end;126        when Atomic_UMAX =>127            if UInt(old_value) > UInt(operand) then return old_value; else return operand; end;128    end;129end;130
131pure func NormalizeAtomicUnsigned(value: Word, size_bytes: integer {1,2,4,8}) => Word132begin133    case size_bytes of134        when 1 => return ZeroExtend{PTO_XLEN}(value[7:0]);135        when 2 => return ZeroExtend{PTO_XLEN}(value[15:0]);136        when 4 => return ZeroExtend{PTO_XLEN}(value[31:0]);137        when 8 => return value;138    end;139end;140
141pure func NormalizeAtomicSigned(value: Word, size_bytes: integer {1,2,4,8}) => Word142begin143    case size_bytes of144        when 1 => return SignExtend{PTO_XLEN}(value[7:0]);145        when 2 => return SignExtend{PTO_XLEN}(value[15:0]);146        when 4 => return SignExtend{PTO_XLEN}(value[31:0]);147        when 8 => return value;148    end;149end;150
151pure func AtomicValueSized(op: AtomicOperation, old_value: Word, operand: Word,152                           size_bytes: integer {1,2,4,8}) => Word153begin154    let old_unsigned = NormalizeAtomicUnsigned(old_value, size_bytes);155    let operand_unsigned = NormalizeAtomicUnsigned(operand, size_bytes);156    let old_signed = NormalizeAtomicSigned(old_value, size_bytes);157    let operand_signed = NormalizeAtomicSigned(operand, size_bytes);158    case op of159        when Atomic_SMIN =>160            if SInt(old_signed) < SInt(operand_signed) then return old_unsigned;161            else return operand_unsigned; end;162        when Atomic_SMAX =>163            if SInt(old_signed) > SInt(operand_signed) then return old_unsigned;164            else return operand_unsigned; end;165        otherwise => return NormalizeAtomicUnsigned(AtomicValue(op, old_unsigned, operand_unsigned), size_bytes);166    end;167end;168
169func AtomicReadModifyWrite(address: Word, size_bytes: integer {1,2,4,8},170                           op: AtomicOperation, operand: Word,171                           order: MemoryOrder) => Word172begin173    let read_probe = ProbeDataAccess(address, size_bytes, size_bytes, FALSE);174    if RaiseDataAccessFault(read_probe, address) then return Zeros{PTO_XLEN}; end;175    let write_probe = ProbeDataAccess(address, size_bytes, size_bytes, TRUE);176    if RaiseDataAccessFault(write_probe, address) then return Zeros{PTO_XLEN}; end;177    if read_probe.translated_address != write_probe.translated_address then178        SetFault(Fault_DataPage, address);179        return Zeros{PTO_XLEN};180    end;181    let old_value = LoadTranslatedUnsigned(182        read_probe.translated_address, size_bytes);183    let new_value = AtomicValueSized(op, old_value, operand, size_bytes);184    StoreTranslated(address, write_probe.translated_address, size_bytes,185        new_value);186    RecordAtomicEvent(write_probe.translated_address, size_bytes, old_value,187        new_value, order, TRUE);188    return old_value;189end;190
191func CompareAndSwap(address: Word, size_bytes: integer {1,2,4,8},192                    expected: Word, desired: Word, order: MemoryOrder) => Word193begin194    let read_probe = ProbeDataAccess(address, size_bytes, size_bytes, FALSE);195    if RaiseDataAccessFault(read_probe, address) then return Zeros{PTO_XLEN}; end;196    let write_probe = ProbeDataAccess(address, size_bytes, size_bytes, TRUE);197    if RaiseDataAccessFault(write_probe, address) then return Zeros{PTO_XLEN}; end;198    if read_probe.translated_address != write_probe.translated_address then199        SetFault(Fault_DataPage, address);200        return Zeros{PTO_XLEN};201    end;202    let old_value = LoadTranslatedUnsigned(203        read_probe.translated_address, size_bytes);204    let succeeds = old_value == NormalizeAtomicUnsigned(expected, size_bytes);205    if succeeds then206        StoreTranslated(address, write_probe.translated_address,207            size_bytes, desired);208    end;209    RecordAtomicEvent(write_probe.translated_address, size_bytes, old_value,210        NormalizeAtomicUnsigned(desired, size_bytes), order, succeeds);211    return old_value;212end;213