What's the purpose of mem_write_ea?

[Timmmm]

It doesn't do anything in the sequential model, and there are zero comments about its purpose. It's also very old and I went far back in Git history to see if I could find comments when it was introduced but I couldn't find any.

I assume it is something to do with formal verification. Does anyone know? What are the expected semantics?

[PeterSewell]

It's needed for the relaxed concurrency semantics (in some forms): it announces to the concurrency model when the effective address is (perhaps speculatively) known and what it is - eg so one can figure out whether some program-order-later instruction is known to be to a disjoint footprint.

…

On Fri, 19 Jan 2024, 09:08 Tim Hutt, ***@***.***> wrote: It doesn't do anything in the sequential model, and there are zero comments about its purpose. It's also very old and I went far back in Git history to see if I could find comments when it was introduced but I couldn't find any. I assume it is something to do with formal verification. Does anyone know? What are the expected semantics? — Reply to this email directly, view it on GitHub <#392>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/ABFMZZQBWXQHN5XVML4DONLYPIZXFAVCNFSM6AAAAABCBTRBK2VHI2DSMVQWIX3LMV43ERDJONRXK43TNFXW4OZWGA4TGOBWGU> . You are receiving this because you are subscribed to this thread.Message ID: ***@***.***>

[Timmmm]

Hmm... but as far as I can see the Sail model always does a mem_write_value() straight after a mem_write_ea() so why have a separate call? I can't find a case where it will call write_ram_ea() but not mem_write_value().

Could you expand for someone who isn't very familiar with the concurrency model or formal verification?

I mean we have this:

      else match translateAddr(vaddr, Write(Data)) {
        TR_Failure(e, _)    => { handle_mem_exception(vaddr, e); RETIRE_FAIL },
        TR_Address(paddr, _) => {
          let eares : MemoryOpResult(unit) = match width {
            BYTE   => mem_write_ea(paddr, 1, aq, rl, false),
            HALF   => mem_write_ea(paddr, 2, aq, rl, false),
            WORD   => mem_write_ea(paddr, 4, aq, rl, false),
            DOUBLE => mem_write_ea(paddr, 8, aq, rl, false)
          };
          match (eares) {
            MemException(e) => { handle_mem_exception(vaddr, e); RETIRE_FAIL },
            MemValue(_) => {
              let rs2_val = X(rs2);
              let res : MemoryOpResult(bool) = match (width) {
                BYTE => mem_write_value(paddr, 1, rs2_val[7..0],  aq, rl, false),
                HALF => mem_write_value(paddr, 2, rs2_val[15..0], aq, rl, false),
                WORD => mem_write_value(paddr, 4, rs2_val[31..0], aq, rl, false),
                DOUBLE if sizeof(xlen) >= 64
                     => mem_write_value(paddr, 8, rs2_val,        aq, rl, false),
                _    => report_invalid_width(__FILE__, __LINE__, width, "store"),
              };
              match (res) {
                MemValue(true)  => RETIRE_SUCCESS,
                MemValue(false) => internal_error(__FILE__, __LINE__, "store got false from mem_write_value"),
                MemException(e) => { handle_mem_exception(vaddr, e); RETIRE_FAIL }
              }
            }
          }
        }
      }

function mem_write_ea (addr, width, aq, rl, con) = {
  if (rl | con) & not(is_aligned_addr(addr, width))
  then MemException(E_SAMO_Addr_Align())
  else match (aq, rl, con) {
    (false, false, false) => MemValue(write_ram_ea(Write_plain, addr, width)),
    (false, true,  false) => MemValue(write_ram_ea(Write_RISCV_release, addr, width)),
    (false, false, true)  => MemValue(write_ram_ea(Write_RISCV_conditional, addr, width)),
    (false, true , true)  => MemValue(write_ram_ea(Write_RISCV_conditional_release, addr, width)),
    (true,  false, false) => throw(Error_not_implemented("store.aq")),
    (true,  true,  false) => MemValue(write_ram_ea(Write_RISCV_strong_release, addr, width)),
    (true,  false, true)  => throw(Error_not_implemented("sc.aq")),
    (true,  true , true)  => MemValue(write_ram_ea(Write_RISCV_conditional_strong_release, addr, width))
  }
}

function mem_write_value (paddr, width, value, aq, rl, con) = {
  mem_write_value_meta(paddr, width, value, default_write_acc, default_meta, aq, rl, con)
}

How is that different to this?

      else match translateAddr(vaddr, Write(Data)) {
        TR_Failure(e, _)    => { handle_mem_exception(vaddr, e); RETIRE_FAIL },
        TR_Address(paddr, _) => {
              let rs2_val = X(rs2);
              let res : MemoryOpResult(bool) = match (width) {
                BYTE => mem_write_value(paddr, 1, rs2_val[7..0],  aq, rl, false),
                HALF => mem_write_value(paddr, 2, rs2_val[15..0], aq, rl, false),
                WORD => mem_write_value(paddr, 4, rs2_val[31..0], aq, rl, false),
                DOUBLE if sizeof(xlen) >= 64
                     => mem_write_value(paddr, 8, rs2_val,        aq, rl, false),
                _    => report_invalid_width(__FILE__, __LINE__, width, "store"),
              };
              match (res) {
                MemValue(true)  => RETIRE_SUCCESS,
                MemValue(false) => internal_error(__FILE__, __LINE__, "store got false from mem_write_value"),
                MemException(e) => { handle_mem_exception(vaddr, e); RETIRE_FAIL }
              }
            }
          }
        }
      }

function mem_write_value (paddr, width, value, aq, rl, con) = {
  if (rl | con) & not(is_aligned_addr(addr, width))
  then MemException(E_SAMO_Addr_Align())
  else {
    match (aq, rl, con) {
      (false, false, false) => write_ram_ea(Write_plain, addr, width),
      (false, true,  false) => write_ram_ea(Write_RISCV_release, addr, width),
      (false, false, true)  => write_ram_ea(Write_RISCV_conditional, addr, width),
      (false, true , true)  => write_ram_ea(Write_RISCV_conditional_release, addr, width),
      (true,  false, false) => throw(Error_not_implemented("store.aq")),
      (true,  true,  false) => write_ram_ea(Write_RISCV_strong_release, addr, width),
      (true,  false, true)  => throw(Error_not_implemented("sc.aq")),
      (true,  true , true)  => write_ram_ea(Write_RISCV_conditional_strong_release, addr, width)
    };
    mem_write_value_meta(paddr, width, value, default_write_acc, default_meta, aq, rl, con)
  }
}

[PeterSewell]

On Sat, 20 Jan 2024 at 19:19, Tim Hutt ***@***.***> wrote: Hmm... but as far as I can see the Sail model always does a mem_write_value() straight after a mem_write_ea() so why have a separate call?

The two are separated by the read of the register that feeds into the value of the write: the mem_write_value() below is (necessarily) after that read, whereas the mem_write_ea() is before it - it's after only the register reads that feed into the address.

…

I can't find a case where it will call write_ram_ea() but *not* mem_write_value(). Could you expand for someone who isn't very familiar with the concurrency model or formal verification? I mean we have this: else match translateAddr(vaddr, Write(Data)) { TR_Failure(e, _) => { handle_mem_exception(vaddr, e); RETIRE_FAIL }, TR_Address(paddr, _) => { let eares : MemoryOpResult(unit) = match width { BYTE => mem_write_ea(paddr, 1, aq, rl, false), HALF => mem_write_ea(paddr, 2, aq, rl, false), WORD => mem_write_ea(paddr, 4, aq, rl, false), DOUBLE => mem_write_ea(paddr, 8, aq, rl, false) }; match (eares) { MemException(e) => { handle_mem_exception(vaddr, e); RETIRE_FAIL }, MemValue(_) => { let rs2_val = X(rs2); let res : MemoryOpResult(bool) = match (width) { BYTE => mem_write_value(paddr, 1, rs2_val[7..0], aq, rl, false), HALF => mem_write_value(paddr, 2, rs2_val[15..0], aq, rl, false), WORD => mem_write_value(paddr, 4, rs2_val[31..0], aq, rl, false), DOUBLE if sizeof(xlen) >= 64 => mem_write_value(paddr, 8, rs2_val, aq, rl, false), _ => report_invalid_width(__FILE__, __LINE__, width, "store"), }; match (res) { MemValue(true) => RETIRE_SUCCESS, MemValue(false) => internal_error(__FILE__, __LINE__, "store got false from mem_write_value"), MemException(e) => { handle_mem_exception(vaddr, e); RETIRE_FAIL } } } } } } function mem_write_ea (addr, width, aq, rl, con) = { if (rl | con) & not(is_aligned_addr(addr, width)) then MemException(E_SAMO_Addr_Align()) else match (aq, rl, con) { (false, false, false) => MemValue(write_ram_ea(Write_plain, addr, width)), (false, true, false) => MemValue(write_ram_ea(Write_RISCV_release, addr, width)), (false, false, true) => MemValue(write_ram_ea(Write_RISCV_conditional, addr, width)), (false, true , true) => MemValue(write_ram_ea(Write_RISCV_conditional_release, addr, width)), (true, false, false) => throw(Error_not_implemented("store.aq")), (true, true, false) => MemValue(write_ram_ea(Write_RISCV_strong_release, addr, width)), (true, false, true) => throw(Error_not_implemented("sc.aq")), (true, true , true) => MemValue(write_ram_ea(Write_RISCV_conditional_strong_release, addr, width)) } } function mem_write_value (paddr, width, value, aq, rl, con) = { mem_write_value_meta(paddr, width, value, default_write_acc, default_meta, aq, rl, con) } How is that different to this? else match translateAddr(vaddr, Write(Data)) { TR_Failure(e, _) => { handle_mem_exception(vaddr, e); RETIRE_FAIL }, TR_Address(paddr, _) => { let rs2_val = X(rs2); let res : MemoryOpResult(bool) = match (width) { BYTE => mem_write_value(paddr, 1, rs2_val[7..0], aq, rl, false), HALF => mem_write_value(paddr, 2, rs2_val[15..0], aq, rl, false), WORD => mem_write_value(paddr, 4, rs2_val[31..0], aq, rl, false), DOUBLE if sizeof(xlen) >= 64 => mem_write_value(paddr, 8, rs2_val, aq, rl, false), _ => report_invalid_width(__FILE__, __LINE__, width, "store"), }; match (res) { MemValue(true) => RETIRE_SUCCESS, MemValue(false) => internal_error(__FILE__, __LINE__, "store got false from mem_write_value"), MemException(e) => { handle_mem_exception(vaddr, e); RETIRE_FAIL } } } } } } function mem_write_value (paddr, width, value, aq, rl, con) = { if (rl | con) & not(is_aligned_addr(addr, width)) then MemException(E_SAMO_Addr_Align()) else { match (aq, rl, con) { (false, false, false) => write_ram_ea(Write_plain, addr, width), (false, true, false) => write_ram_ea(Write_RISCV_release, addr, width), (false, false, true) => write_ram_ea(Write_RISCV_conditional, addr, width), (false, true , true) => write_ram_ea(Write_RISCV_conditional_release, addr, width), (true, false, false) => throw(Error_not_implemented("store.aq")), (true, true, false) => write_ram_ea(Write_RISCV_strong_release, addr, width), (true, false, true) => throw(Error_not_implemented("sc.aq")), (true, true , true) => write_ram_ea(Write_RISCV_conditional_strong_release, addr, width) }; mem_write_value_meta(paddr, width, value, default_write_acc, default_meta, aq, rl, con) } } — Reply to this email directly, view it on GitHub <#392 (reply in thread)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/ABFMZZURPDXGJYPR3CWXN63YPQKCZAVCNFSM6AAAAABCBTRBK2VHI2DSMVQWIX3LMV43SRDJONRXK43TNFXW4Q3PNVWWK3TUHM4DCOJSHAYDO> . You are receiving this because you commented.Message ID: ***@***.***>

[Timmmm]

I'm working on fixing #49 - how would you expect mem_write_ea() to be called when we have two physical addresses?

The requirement for inserting the register read between the address translation and actual write is quite a pain. Otherwise I would just have a single mem_write() function that takes a virtual address and the value to write and takes care of everything. But since Sail doesn't support first class functions I can't insert the register read in the right place. Hmm.