Skip to content

Memory Semantics

Jump to bottom
Sandeep Dasgupta edited this page May 11, 2018 · 4 revisions

Table Of Contents

  • Design & Implementation
    • Some abstractions
    • Allocation
    • Write
    • Reads
  • Stack Layout
  • Text Section layout

Some abstraction

  • AbstractValue: The value stored in stack slots. To be defined by the client.

  • memValue(N: #elems, Sz: Size of elem, D:MemData) where MemData (List{AbstractValue})

    • This abstraction is what is consumed by all the low level api's like mAlloc, mWrite

  • MInt and MIntMap ::= mintmap(Map) are the sorts of the user level data that are stored in memory. That means they are first need to be converted to MemData.

  • toMemData is an overloaded K function used for converting a MInt or MIntMap to MemData.

    • Used by apls like storeToMeory and mAlloc to split Data (MInt or MIntMap) to byte level chunks

    • toMemData(MInt, Nbits, ResultMemData)

      • Assumptions: Nbits == bitwidthMInt(MInt)
      • Split Mint to 8 bit chunks.
      • Eg: toMemData(MI, 32, .MemData) results in byte(0, MI), byte(1, MI), byte(2, MI), byte(3, MI)

    • toMemData(MIntMap, Nbits, ResultMemData)

      • Assumptions: bitwidthMInt(MIntMap[0]) * size(MIntMap) == Nbits
      • For each element of MIntMap, call toMemData.
      • Eg: toMemData({0 -> mi(64, I1) 1 -> mi(64, I2)}, 2*8*8, .MemData) results in byte(0, mi(64, I1)), byte(1, mi(64, I1)), byte(2, mi(64, I1)), byte(3, mi(64, I1)) byte(0, mi(64, I2)), byte(1, mi(64, I2)), byte(2, mi(64, I2)), byte(3, mi(64, I2))

Allocation

 symloc(ID, A)  <-- allocateStackMemory(N:Number of slots allocated, A: Alignment)
 symloc(ID, A)  <-- allocateLocalMemory(N:Number of slots allocated, A: Alignment)

  • ID is an identifier to access the internal representation of memory.

  • Allocated memory is byte addressable.

  • AllocateStackMemory

    • Used for allocating stack memory and saving the stack base address.
    • We store ID in cell <stackbase> to later read/writes/free.
    • N ::= Environment Memory (upper 64 slots) + Stack Memory (Rest)
    • Uses makeUndefMIntMap(N) which creates N 1 byte undef and return a Map storing them in byte granularity, which are then store in memory.

  • Within the allocated memory, we access the individual bytes using offsets.

Clone this wiki locally