var address : bits(64); var data : bits(16); let privileged : boolean = PSTATE.EL != EL0; let accdesc : AccessDescriptor = CreateAccDescExLDST(MemOp_STORE, acqrel, tagchecked, privileged, t); if n == 31 then CheckSPAlignment(); address = SP{64}(); elsif rn_unknown then address = ARBITRARY : bits(64); else address = X{64}(n); end; if rt_unknown then data = ARBITRARY : bits(16); else data = X{16}(t); end; var status : bit = '1'; // Check whether the Exclusives monitors are set to include the // physical memory locations corresponding to virtual address // range [address, address+dbytes-1]. // If AArch64_ExclusiveMonitorsPass() returns FALSE and the memory address, // if accessed, would generate a synchronous Data Abort exception, it is // IMPLEMENTATION DEFINED whether the exception is generated. // It is a limitation of this model that synchronous Data Aborts are never // generated in this case, as Mem is not called. // If FEAT_SPE is implemented, it is also IMPLEMENTATION DEFINED whether or not the // physical address packet is output when permitted and when // AArch64_ExclusiveMonitorPass() returns FALSE for a Store Exclusive instruction. // This behavior is not reflected here due to the previously stated limitation. if AArch64_ExclusiveMonitorsPass(address, 2, accdesc) then // This atomic write will be rejected if it does not refer // to the same physical locations after address translation. Mem{16}(address, accdesc) = data; status = ExclusiveMonitorsStatus(); end; X{32}(s) = ZeroExtend{32}(status);