module Platform.AArch64.PublicationRoutine

import Compiler.MachineAArch64
import Compiler.MachineAArch64Assembly
import Model.Config

-- The AAPCS64 twin of Runtime.NativePhysicalTrainingRoutine's Publish32:
-- x0 points to GPPut, w1 is its new value, x2 points to the doorbell, w3 is
-- the submit token. DSB SY completes preceding normal-memory writes before
-- the device-memory doorbell store. A second host thread is not involved.
-- The barrier's encoding is checked separately; single-thread test output
-- cannot establish this ordering property on a GPU.
def aarch64Publish32Assembly : (family AArch64Assembly) =
  (constructor AArch64Assembly AArch64AssemblyEmit
    (constructor AArch64Instruction AArch64StoreMemory32
      (constructor AArch64Register AArch64X0) 0 (constructor AArch64Register AArch64X1))
    (constructor AArch64Assembly AArch64AssemblyEmit
      (constructor AArch64Instruction AArch64DataSynchronizationBarrierSystem)
      (constructor AArch64Assembly AArch64AssemblyEmit
        (constructor AArch64Instruction AArch64StoreMemory32
          (constructor AArch64Register AArch64X2) 0 (constructor AArch64Register AArch64X3))
        (constructor AArch64Assembly AArch64AssemblyEmit
          (constructor AArch64Instruction AArch64MoveWideZero
            (constructor AArch64Register AArch64X0) 0 (constructor AArch64HalfwordShift AArch64Shift0))
          (constructor AArch64Assembly AArch64AssemblyEmit
            (constructor AArch64Instruction AArch64Return)
            (constructor AArch64Assembly AArch64AssemblyEnd))))))

def aarch64Publish32Routine : Bytes =
  (eliminate AArch64AssemblyResult (lambda unrestricted result : (family AArch64AssemblyResult) . Bytes)
    (aarch64Assemble aarch64Publish32Assembly)
    (branch AArch64AssemblyEncoded code . code)
    (branch AArch64AssemblyEncodeDuplicateLabel name . b"")
    (branch AArch64AssemblyMissingLabel name . b"")
    (branch AArch64AssemblyDisplacementOutOfRange name . b"")
    (branch AArch64AssemblyOperandRefused value . b""))