Why do writes to memory-mapped registers return MemoryOpResult(bool)?

[Furetur]

Hello! Just a quick question.

Why do functions clint_store and htif_store that specify writes to memory-mapped registers return MemoryOpResult(bool) and not MemoryOpResult(unit)? As far as I can tell, all memory-mapped modules (CLINT and HTIF) never return Ok(false). However, I'm fairly new to hardware design, so I might be overlooking something.

[Alasdair]

I think the bool was intended to represent success/failure of an exclusive or CAS operation, but in practice we haven't ended up using it.

The current sail memory write interface uses the type result(option(bool), 'abort) so:

• Ok(None()) = successful regular memory access
• Ok(Some(true)) = write exclusive success (in theory)
• Err(<some external abort>) = external memory abort (with architecture specific type)

You timed this question quite nicely though, as we actually had a meeting just yesterday where we talked about simplifying to result(unit, 'abort)/option('abort) in the future.

[Timmmm]

Yeah I've wondered this since false is never actually returned. If it were it would be used in Store-Conditional:

                    match mem_write_value(addr, width_bytes, rs2_val[width_bytes * 8 - 1 .. 0], aq & rl, rl, true) {
                      Ok(true)  => { X(rd) = zero_extend(0b0); cancel_reservation(); RETIRE_SUCCESS },
                      Ok(false) => { X(rd) = zero_extend(0b1); cancel_reservation(); RETIRE_SUCCESS },
                      Err(e)    => { handle_mem_exception(vaddr, e); RETIRE_FAIL }
                    }

So in theory you could make your memory system fail store conditionals by returning false. In our version we did that by overriding speculate_conditional() instead though (and moved it to a more sensible place - see #681. That was mostly because it looked like the obvious way to do it and at the time I didn't understand this.

Doing it via the mem_write_value() result is maybe more correct because it happens after PMP/PMA checks, although the spec is as vague as usual about how they interact. It only says:

For the purposes of memory protection, a failed SC.W may be treated like a store.

I think we should keep it for now, and when we add a proper library interface we expose the capability to fail SC stores on each step.

[Furetur]

Thank you for such a detailed explanation!