diff options
Diffstat (limited to 'risc-v/riscv_extras_embed.lem')
| -rw-r--r-- | risc-v/riscv_extras_embed.lem | 19 |
1 files changed, 17 insertions, 2 deletions
diff --git a/risc-v/riscv_extras_embed.lem b/risc-v/riscv_extras_embed.lem index 3f04f9a2..d89dc44c 100644 --- a/risc-v/riscv_extras_embed.lem +++ b/risc-v/riscv_extras_embed.lem @@ -6,33 +6,48 @@ open import Prompt val MEMr : (vector bitU * integer) -> M (vector bitU) val MEMr_acquire : (vector bitU * integer) -> M (vector bitU) +val MEMr_strong_acquire : (vector bitU * integer) -> M (vector bitU) val MEMr_reserved : (vector bitU * integer) -> M (vector bitU) val MEMr_reserved_acquire : (vector bitU * integer) -> M (vector bitU) +val MEMr_reserved_strong_acquire : (vector bitU * integer) -> M (vector bitU) let MEMr (addr,size) = read_mem false Read_plain addr size let MEMr_acquire (addr,size) = read_mem false Read_RISCV_acquire addr size +let MEMr_strong_acquire (addr,size) = read_mem false Read_RISCV_strong_acquire addr size let MEMr_reserved (addr,size) = read_mem false Read_RISCV_reserved addr size let MEMr_reserved_acquire (addr,size) = read_mem false Read_RISCV_reserved_acquire addr size +let MEMr_reserved_strong_acquire (addr,size) + = read_mem false Read_RISCV_reserved_strong_acquire addr size val MEMea : (vector bitU * integer) -> M unit val MEMea_release : (vector bitU * integer) -> M unit +val MEMea_strong_release : (vector bitU * integer) -> M unit val MEMea_conditional : (vector bitU * integer) -> M unit val MEMea_conditional_release : (vector bitU * integer) -> M unit +val MEMea_conditional_strong_release : (vector bitU * integer) -> M unit let MEMea (addr,size) = write_mem_ea Write_plain addr size let MEMea_release (addr,size) = write_mem_ea Write_RISCV_release addr size +let MEMea_strong_release (addr,size) = write_mem_ea Write_RISCV_strong_release addr size let MEMea_conditional (addr,size) = write_mem_ea Write_RISCV_conditional addr size let MEMea_conditional_release (addr,size) = write_mem_ea Write_RISCV_conditional_release addr size +let MEMea_conditional_strong_release (addr,size) + = write_mem_ea Write_RISCV_conditional_strong_release addr size val MEMval : (vector bitU * integer * vector bitU) -> M unit val MEMval_release : (vector bitU * integer * vector bitU) -> M unit +val MEMval_strong_release : (vector bitU * integer * vector bitU) -> M unit val MEMval_conditional : (vector bitU * integer * vector bitU) -> M unit val MEMval_conditional_release : (vector bitU * integer * vector bitU) -> M unit +val MEMval_conditional_strong_release : (vector bitU * integer * vector bitU) -> M unit let MEMval (_,_,v) = write_mem_val v >>= fun _ -> return () let MEMval_release (_,_,v) = write_mem_val v >>= fun _ -> return () -let MEMval_conditional (_,_,v) = write_mem_val v >>= fun _ -> return () (* (if b then B1 else B0) *) -let MEMval_conditional_release (_,_,v) = write_mem_val v >>= fun _ -> return () (* (if b then B1 else B0) *) +let MEMval_strong_release (_,_,v) = write_mem_val v >>= fun _ -> return () +let MEMval_conditional (_,_,v) = write_mem_val v >>= fun _ -> return () +let MEMval_conditional_release (_,_,v) = write_mem_val v >>= fun _ -> return () +let MEMval_conditional_strong_release (_,_,v) + = write_mem_val v >>= fun _ -> return () let speculate_conditional_success () = excl_result () >>= fun b -> return (if b then B1 else B0) |