ddc-code-0.4.2.1: salt/runtime64/Object.dcs
-- | Primitives for constructing and destructing 64-bit heap objects.
--
-- IMPORTANT: Only one of 'Object64' or 'Object32' is linked into the DDC
-- runtime system. It is also the /only/ module that knows about the layout
-- of heap objects. All access to heap objects must go through the interface
-- provided by this module.
--
-- All 64-bit heap objects start with a 32-bit word containing the constructor
-- tag of the object and a format field in the least-significant byte.
--
-- OBJECT
-- ~~~~~~
-- byte 3 2 1 0 (in MSB order)
-- TAG2 TAG1 TAG0 FORMAT ...
--
--
-- FORMAT field
-- ~~~~~~~~~~~~
-- bit 7 6 5 4 3 2 1 0
-- -- arg --- -- obj ---
-- X X X X X X 0 0 -- Forward / Broken-Heart
-- X X X X a X X X -- Anchor flag
-- 0 0 0 1 a 0 0 1 -- Thunk
-- 0 0 1 0 a 0 0 1 -- DataBoxed
-- 0 0 1 1 a 0 0 1 -- DataRaw
-- 0 1 0 0 a 0 0 1 -- DataMixed
-- 0 1 0 1 a 0 0 1 -- SuspIndir
-- -- size -- a 0 1 1 -- DataRawSmall
--
-- Data GC Forwarding / Broken-Heart pointers.
-- During garbage collection, after the GC copies an object to the
-- "to-space" its header in the "from-space" is overwritten with a pointer
-- to where the "to-space" version of the object is.
--
-- We can identify these pointers because their lowest 2 bits are always 00.
-- This is because objects in the heap are always 4-byte aligned.
--
-- For all other values of the format field, we ensure the lowest two bits
-- are not 00.
--
-- Data Anchor flag
-- If bit 3 in the format field is set then the GC is not permitted to move
-- the object. This is useful when the object has been allocated by malloc
-- and exists outside the DDC runtime's garbage collected heap.
--
-- Data Data{Boxed, Mixed, Raw, RawSmall}
-- There are four data object formats:
-- DataBoxed: A boxed object containing pointers to more heap objects.
-- DataMixed: Some heap pointers, and some raw data.
-- DataRaw: Contains raw data and no pointers.
-- DataRawSmall: Contains raw data where the size is small enough to
-- encode directly in the format field.
--
-- The -obj- (object mode) portion of the format field can be used to
-- determine if the object is a forwarding pointer, has a fixed value for
-- its format field, or is a DataRS object.
--
-- Note: 64-bit floats.
-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~
-- The various object formats always contain an even number of 32-bit words
-- in the header portion, before the payload. This ensures that the payloads
-- of all heap objects are 8-byte aligned. We do this to support architectures
-- that cannot load misaligned double precision floats (Float64). Architectures
-- that can load them typically suffer a penalty, so it is good to align heap
-- objects anyway.
--
module Runtime.Object
export value
-- Get the tag of an object.
getTag : [r: Region]. Ptr# r Obj -> Tag#
-- Thunk initialization.
allocThunk : [r1: Region]. Addr# -> Nat# -> Nat# -> Nat# -> Nat# -> Ptr# r1 Obj
copyThunk : [r1 r2: Region]. Ptr# r1 Obj -> Ptr# r2 Obj -> Nat# -> Nat# -> Ptr# r2 Obj
extendThunk : [r1 r2: Region]. Ptr# r1 Obj -> Nat# -> Ptr# r2 Obj
funThunk : [r1: Region]. Ptr# r1 Obj -> Addr#
paramsThunk : [r1: Region]. Ptr# r1 Obj -> Nat#
boxesThunk : [r1: Region]. Ptr# r1 Obj -> Nat#
argsThunk : [r1: Region]. Ptr# r1 Obj -> Nat#
runsThunk : [r1: Region]. Ptr# r1 Obj -> Nat#
setThunk : [r1 r2: Region]. Ptr# r1 Obj -> Nat# -> Nat# -> Ptr# r2 Obj -> Void#
getThunk : [r1 r2: Region]. Ptr# r1 Obj -> Nat# -> Ptr# r2 Obj
-- Objects with just pointers to boxed things.
allocBoxed : [r1: Region]. Tag# -> Nat# -> Ptr# r1 Obj
getBoxed : [r1 r2: Region]. Ptr# r1 Obj -> Nat# -> Ptr# r2 Obj
setBoxed : [r1 r2: Region]. Ptr# r1 Obj -> Nat# -> Ptr# r2 Obj -> Void#
-- Object with mixed pointers and raw, non-pointer data.
allocMixed : [r1: Region]. Tag# -> Nat# -> Nat# -> Ptr# r1 Obj
getMixed : [r1 r2: Region]. Ptr# r1 Obj -> Nat# -> Ptr# r2 Obj
payloadMixed : [r1: Region]. Ptr# r1 Obj -> Ptr# r1 Word8#
-- Objects containing raw non-pointer data.
allocRaw : [r1: Region]. Tag# -> Nat# -> Ptr# r1 Obj
payloadRaw : [r1: Region]. Ptr# r1 Obj -> Ptr# r1 Word8#
payloadSizeRaw : [r1: Region]. Ptr# r1 Obj -> Nat#
-- Objects with small, raw non-pointer data.
allocSmall : [r1: Region]. Tag# -> Nat# -> Ptr# r1 Obj
payloadSmall : [r1: Region]. Ptr# r1 Obj -> Ptr# r1 Word8#
with letrec
-- | Get the constructor tag of an object.
getTag [r: Region] (obj: Ptr# r Obj): Tag#
= do
ptr = castPtr# obj
header = peek# ptr 0#
tag32 = shr# header 8w32#
promote# tag32
-- Thunk ----------------------------------------------------------------------
-- | Allocate a Thunk
-- The payload contains a code pointer to the top-level supercombinator,
-- along with pointers to any available arguments. The actual pointer values
-- for the arguments are undefined.
--
-- Note that unlike the GHC runtime we don't use a separate PAP
-- (Partial Application) object type to store partially applied arguments.
-- To perform a partial application we just create a new Thunk, copy the old
-- arguments into it, and write the extra partially applied arguments into the
-- new thunk. This is done to keep the implementation complexity down, and we
-- haven't performed any concrete performance comparisons between the two
-- approaches.
--
-- For the GHC approach see:
-- How to make a fast curry, push/enter vs eval apply.
-- Simon Marlow and Simon Peyton Jones.
-- Journal of Functional Programming, 2006.
--
-- A thunk wraps a top-level super of the following form:
-- f = /\a1 .. /\an. \x1 .. \xn. box .. box. body
--
-- The type parameters a1 .. an are not represented at runtime.
--
-- The value parameters x1 .. xn are counted in the boxes field.
-- We need to collect this many applied arguments in the thunk before
-- we can call the super.
--
-- The boxes box .. box are counted in the boxes field of the thunk.
-- We need to run the thunk this many times before calling the super.
-- the expression 'box body' is equivalent to (\(_ : Void#). body),
-- and running it eliminates the outer lambda.
--
-- typedef struct
-- { uint32_t tagFormat; // Constructor tag and format field.
-- uint8_t params; // Value parameters of super.
-- uint8_t boxes; // Number of runs required.
-- uint8_t args; // Available arguments.
-- uint8_t runs; // Number of times we've been run so far.
-- Fun* fun; // Function pointer.
-- Obj* payload[]; // Pointers to available arguments.
-- } Thunk;
--
allocThunk [r: Region] (fun: Addr#)
(params: Nat#) (boxes: Nat#)
(args: Nat#) (runs: Nat#)
: Ptr# r Obj
= do
-- The payload needs to be big enough to store pointers to the
-- current available args.
bytesPayload = shl# args (size2# [Addr#])
bytesObj = add# (size# [Word32#]) -- tagFormat word.
(add# (size# [Word32#]) -- params/boxes/args/runs.
(add# (size# [Word64#]) -- function pointer.
bytesPayload)) -- function args.
case check# bytesObj of
True# -> allocThunk_ok fun params boxes args runs bytesObj
False# -> fail#
allocThunk_ok [r: Region] (fun: Addr#)
(params: Nat#) (boxes: Nat#)
(args: Nat#) (runs: Nat#)
(bytesObj: Nat#)
: Ptr# r Obj
= do
addr = alloc# bytesObj
-- The tag of thunks is set to all 1 bits to make them easy to identify.
tag32 = 0xffffff00w32#
format = 0b00010001w32#
header = bor# tag32 format
write# addr 0# header
-- Truncate params to 8-bits and write to object.
params8 = truncate# [Word8#] [Nat#] params
write# addr 4# params8
-- Truncate boxes to 8-bits and write to object.
boxes8 = truncate# [Word8#] [Nat#] boxes
write# addr 5# boxes8
-- Truncate args count to 8-bits and write to object.
args8 = truncate# [Word8#] [Nat#] args
write# addr 6# args8
-- Truncate runs count to 8-bits and write to object.
runs8 = truncate# [Word8#] [Nat#] runs
write# addr 7# runs8
-- Write the function pointer.
write# addr 8# fun
makePtr# addr
-- | Copy the available arguments from one thunk to another.
copyThunk
[rSrc rDst: Region]
(src: Ptr# rSrc Obj) (dst: Ptr# rDst Obj)
(index: Nat#) (len: Nat#)
: Ptr# rDst Obj
= case ge# index len of
True# -> dst
False#
-> do ptr = getThunk src index
setThunk dst 0# index ptr
copyThunk src dst (add# index 1#) len
-- | Copy a thunk while extending the number of available argument slots.
-- This is used when implementing both the curryN# and applyN# core primops.
extendThunk
[rSrc rDst: Region]
(src: Ptr# rSrc Obj) (more: Nat#)
: Ptr# rDst Obj
= do
-- Function pointer and arity of that function.
fun = funThunk src
params = paramsThunk src
boxes = boxesThunk src
-- Available arguments in source and destination.
args = argsThunk src
args' = add# args more
-- Number of times the thunk has been run
runs = runsThunk src
-- Allocate a new thunk with the orignal function and arity.
dst = allocThunk [rDst] (funThunk src) params boxes args' runs
-- Copy argument pointers from the source into the new thunk.
copyThunk src dst 0# args
-- | Get the function pointer from a thunk.
funThunk [r: Region] (obj: Ptr# r Obj): Addr#
= read# [Addr#] (takePtr# obj) 8#
-- | Get the arity of the function in a thunk.
paramsThunk [r: Region] (obj: Ptr# r Obj): Nat#
= promote# (read# [Word8#] (takePtr# obj) 4#)
-- | Get the count of available arguments in a thunk.
boxesThunk [r: Region] (obj: Ptr# r Obj): Nat#
= promote# (read# [Word8#] (takePtr# obj) 5#)
-- | Get the count of available arguments in a thunk.
argsThunk [r: Region] (obj: Ptr# r Obj): Nat#
= promote# (read# [Word8#] (takePtr# obj) 6#)
-- | Get the count of available arguments in a thunk.
runsThunk [r: Region] (obj: Ptr# r Obj): Nat#
= promote# (read# [Word8#] (takePtr# obj) 7#)
-- | Set one of the pointers in a thunk.
-- The value is just a plain Addr# because we don't know what region the
-- original pointer in the Thunk was pointing to. Also, when setting these
-- pointers for the first time the pointer values in the thunk are undefined.
-- This takes a 'base' and 'offset' parameter separately to allow for easier
-- code generation.
setThunk
[r1 r2: Region]
(obj: Ptr# r1 Obj) (base: Nat#) (offset: Nat#) (val: Ptr# r2 Obj): Void#
= write# (takePtr# obj)
(add# 16# (shl# (add# base offset) (size2# [Addr#])))
(takePtr# val)
-- | Get one of the arguments from a thunk.
getThunk
[r1 r2: Region]
(obj: Ptr# r1 Obj) (index: Nat#): Ptr# r2 Obj
= read# (takePtr# obj)
(add# 16# (shl# index (size2# [Addr#])))
-- Boxed ----------------------------------------------------------------------
-- | Allocate a Boxed Data Object.
-- The payload contains pointers to other heap objects.
--
-- The arity must be no greater than 2^32, else undefined.
-- This object type is typically used for algebraic data, which won't have
-- more than 2^32 fields.
--
-- typedef struct
-- { uint32_t tagFormat; // Constructor tag and format field.
-- uint32_t arity; // Arity of the data constructor.
-- // (The number of pointers in the payload)
-- ObjData payload[];
-- } DataBoxed;
--
allocBoxed
[r: Region]
(tag: Tag#) (arity: Nat#): Ptr# r Obj
= do
-- Multiple arity by 8 bytes-per-pointer to get size of payload.
bytesPayload = shl# arity (size2# [Addr#])
bytesObj = add# (size# [Word32#])
(add# (size# [Word32#]) bytesPayload)
case check# bytesObj of
True# -> allocBoxed_ok tag arity bytesObj
False# -> fail#
allocBoxed_ok
[r: Region]
(tag: Tag#) (arity: Nat#) (bytesObj: Nat#): Ptr# r Obj
= do
addr = alloc# bytesObj
tag32 = promote# [Word32#] [Tag#] tag
format = 0b00100001w32#
header = bor# (shl# tag32 8w32#) format
write# addr 0# header
-- Truncate arity to 32-bits.
arity32 = truncate# [Word32#] [Nat#] arity
write# addr 4# arity32
makePtr# addr
---- | Get one of the pointers from a boxed data object.
getBoxed
[r1 r2: Region]
(obj: Ptr# r1 Obj) (index: Nat#)
: Ptr# r2 Obj
= read# (takePtr# obj)
(add# 8# (shl# index (size2# [Addr#])))
-- | Set one of the pointers from a boxed data object.
setBoxed
[r1 r2: Region]
(obj: Ptr# r1 Obj) (index: Nat#) (val: Ptr# r2 Obj): Void#
= write# (takePtr# obj)
(add# 8# (shl# index (size2# [Addr#])))
val
-- Mixed ----------------------------------------------------------------------
-- | Allocate a Mixed Data Object.
-- The payload contains some pointers followed by raw data.
--
-- The arity (ptrCount) must be no greater than 2^32, else undefined.
-- The payload can have length up to 2^64.
--
-- typedef struct
-- { uint32_t tagFormat;
-- uint32_t ptrCount; // Number of pointers at the start of the payload.
-- uint64_t size; // Size of the whole object, in bytes.
-- ObjData payload[]; // Contains ptrCount pointers, then raw data.
-- } DataMixed;
--
allocMixed
[r: Region]
(tag: Tag#) (arity: Nat#) (bytesRaw: Nat#)
: Ptr# r Obj
= do
bytesPtrs = shl# arity 3#
bytesObj = add# (size# [Word32#])
(add# (size# [Word32#])
(add# (size# [Word64#])
(add# bytesPtrs bytesRaw)))
case check# bytesObj of
True# -> allocMixed_ok [r] tag arity bytesObj
False# -> fail# [Ptr# r Obj]
allocMixed_ok
[r: Region]
(tag: Tag#) (arity: Nat#) (bytesObj: Nat#)
: Ptr# r Obj
= do
addr = alloc# bytesObj
tag32 = promote# tag
format = 0b01000001w32#
header = bor# (shl# tag32 8w32#) format
write# addr 0# header
arity32 = truncate# [Word32#] [Nat#] arity
write# addr 4# arity32
bytesObj32 = promote# [Word64#] [Nat#] bytesObj
write# addr 8# bytesObj32
makePtr# addr
-- | Get one of the pointers from a mixed data object.
getMixed [r1 r2: Region] (obj: Ptr# r1 Obj) (index: Nat#): Ptr# r2 Obj
= read# (takePtr# obj)
(add# 16# (shl# index (size2# [Addr#])))
-- | Get the address of the raw data payload from a mixed object.
payloadMixed [r: Region] (obj: Ptr# r Obj): Ptr# r Word8#
= plusPtr# (castPtr# obj) 16#
-- Raw ------------------------------------------------------------------------
-- | A Raw Data Object.
-- A raw data object does not contain heap pointers that need to be traced
-- by the garbage collector.
--
-- The payload size must be no greater than (2^32 - 8), else undefined.
--
-- typedef struct
-- { uint32_t tagFormat; // Constructor tag and format field.
-- uint32_t size; // Size of the whole object, in bytes.
-- uint8_t payload[]; // Raw data that does not contain heap pointers.
-- } DataRaw;
--
allocRaw
[r: Region] (tag: Tag#) (bytesPayload: Nat#): Ptr# r Obj
= do
bytesObj = add# (size# [Word32#])
(add# (size# [Word32#]) bytesPayload)
case check# bytesObj of
True# -> allocRaw_ok tag bytesObj
False# -> fail#
allocRaw_ok
[r: Region] (tag: Tag#) (bytesObj: Nat#): Ptr# r Obj
= do
addr = alloc# bytesObj
tag32 = promote# tag
format = 0b00110001w32#
header = bor# (shl# tag32 8w32#) format
write# addr 0# header
bytesObj32 = truncate# [Word32#] [Nat#] bytesObj
write# addr 4# bytesObj32
makePtr# addr
-- | Get the payload data from a raw object.
payloadRaw [r: Region] (obj: Ptr# r Obj): Ptr# r Word8#
= plusPtr# (castPtr# obj) 8#
-- | Get the size of the payload of a raw object, in bytes.
payloadSizeRaw [r: Region] (obj: Ptr# r Obj): Nat#
= promote# (read# [Word32#] (takePtr# obj) 4#)
-- RawSmall -------------------------------------------------------------------
-- | A Small Raw object.
-- The object size is encoded as part of format field
-- This saves us from needing to include a separate arity field.
--
-- The payload size must be no greater than 16 words, else undefined.
--
-- typedef struct
-- { uint32_t tagFormat; // Constructor tag and format field.
-- uint8_t payload[]; // Raw data that does not contain heap pointers.
-- } DataRawSmall;
--
allocSmall
[r: Region]
(tag: Tag#) (bytesPayload: Nat#): Ptr# r Obj
= do
bytesObj = add# 4# bytesPayload
case check# bytesObj of
True# -> allocSmall_ok tag bytesPayload bytesObj
False# -> fail#
allocSmall_ok
[r: Region]
(tag: Tag#) (bytesPayload: Nat#) (bytesObj: Nat#): Ptr# r Obj
= do
addr = alloc# bytesObj
tag32 = promote# tag
bytesPayload32 = truncate# bytesPayload
wordsPayload32 = shr# bytesPayload32 2w32#
format = 0b0011w32#
header = bor# (shl# tag32 8w32#)
(bor# (shl# wordsPayload32 4w32#) format)
write# addr 0# header
makePtr# addr
-- | Get the payload data from a raw small object.
payloadSmall [r: Region] (obj: Ptr# r Obj): Ptr# r Word8#
= plusPtr# (castPtr# obj) 4#