Theory TSO_Code_Gen

(*<*)
theory TSO_Code_Gen
imports
  TSO
begin

(*>*)
subsection ‹ Code generator setup for TSO \label{sec:tso-code_generation} ›

text‹

The following is only sound if the generated code runs on a machine with a TSO memory model such as:
 ▪ x86
 ▪ x86 code running on macOS under Rosetta 2 (ask Google)

Notes:
 ▪ Haskell: GHC exposes unfenced operations for references and some kinds of arrays
  ▪ GHC has a zoo of arrays; for now we use the general but inefficient boxed array type
 ▪ SML: Poly/ML appears to have committed to release/acquire (see email with subject ``Git master update: ARM64, PIE and new bootstrap process'')
  ▪ on x86 this is TSO
 ▪ Scala: beyond the scope of this work

TODO:
 ▪ support a ▩‹CAS›-like operation
  ▪ Haskell: 🌐‹https://stackoverflow.com/questions/10102881/haskell-how-does-atomicmodifyioref-work›

›


subsubsection ‹Haskell›

text‹

Adaption layer

›

code_printing code_module "TSOHeap" ⇀ (Haskell)
‹
module TSOHeap (
    TSO
  , IORef, newIORef, readIORef, writeIORef
  , Array, newArray, newListArray, newFunArray, lengthArray, readArray, writeArray
  , parallel
  ) where

import Control.Concurrent (forkIO)
import qualified Control.Concurrent.MVar as MVar
import qualified Data.Array.IO as Array -- FIXME boxed, contemplate the menagerie of other arrays; perhaps type families might help here
import Data.IORef (IORef, newIORef, readIORef, writeIORef)
import Data.List (genericLength)

type TSO a = IO a
type Array a = Array.IOArray Integer a
type Ref a = Data.IORef.IORef a

writeIORef :: IORef a -> a -> IO ()
writeIORef = writeIORef -- FIXME strict variant?

newArray :: Integer -> a -> IO (Array a)
newArray k = Array.newArray (0, k - 1)

newListArray :: [a] -> IO (Array a)
newListArray xs = Array.newListArray (0, genericLength xs - 1) xs

newFunArray :: Integer -> (Integer -> a) -> IO (Array a)
newFunArray k f = Array.newListArray (0, k - 1) (map f [0..k-1])

lengthArray :: Array a -> IO Integer
lengthArray a = Array.getBounds a >>= return . (\(_, l) -> l + 1)

readArray :: Array a -> Integer -> IO a
readArray = Array.readArray

writeArray :: Array a -> Integer -> a -> IO ()
writeArray = Array.writeArray

-- note we don't want "forkFinally" as we don't model exceptions
parallel :: IO () -> IO () -> IO ()
parallel p q = do
  mvar <- MVar.newEmptyMVar
  forkIO (p >> MVar.putMVar mvar ()) -- FIXME putMVar is lazy
  b <- q
  a <- MVar.takeMVar mvar
  return ()
›

code_reserved Haskell TSOHeap

text ‹Monad›

code_printing type_constructor tso ⇀ (Haskell) "TSOHeap.TSO _"
code_monad tso.bind Haskell
code_printing constant tso.return ⇀ (Haskell) "return"
code_printing constant tso.raise ⇀ (Haskell) "error"
code_printing constant tso.parallel ⇀ (Haskell) "TSOHeap.parallel"

text ‹Intermediate operation avoids invariance problem in ‹Scala› (similar to value restriction)›

setup ‹Sign.mandatory_path "tso.Ref"›

definition ref' where
  [code del]: "ref' = tso.Ref.ref"

lemma [code]:
  "tso.Ref.ref x = tso.Ref.ref' x"
  by (simp add: tso.Ref.ref'_def)

setup ‹Sign.parent_path›

text ‹Haskell›

code_printing type_constructor ref ⇀ (Haskell) "TSOHeap.Ref _"
code_printing constant Ref ⇀ (Haskell) "error/ \"bare Ref\""
code_printing constant tso.Ref.ref' ⇀ (Haskell) "TSOHeap.newIORef"
code_printing constant tso.Ref.lookup ⇀ (Haskell) "TSOHeap.readIORef"
code_printing constant tso.Ref.update ⇀ (Haskell) "TSOHeap.writeIORef"
code_printing constant "HOL.equal :: 'a ref ⇒ 'a ref ⇒ bool" ⇀ (Haskell) infix 4 "=="
code_printing class_instance ref :: HOL.equal ⇀ (Haskell) -

(*<*)

end
(*>*)