bits(64) address; bits(16) data; AccessDescriptor accdesc = CreateAccDescExLDST(MemOp_STORE, FALSE, tagchecked); if n == 31 then CheckSPAlignment(); address = SP[]; elsif rn_unknown then address = bits(64) UNKNOWN; else address = X[n, 64]; if rt_unknown then data = bits(16) UNKNOWN; else data = X[t, 16]; bit status = '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[address, 2, accdesc] = data; status = ExclusiveMonitorsStatus(); X[s, 32] = ZeroExtend(status, 32);