diff options
| author | Shaked Flur | 2017-09-03 15:05:23 +0100 |
|---|---|---|
| committer | Shaked Flur | 2017-09-03 15:05:23 +0100 |
| commit | 75022d46352525305b4c06b4988bf2df15f9f29e (patch) | |
| tree | ee2f171e2c36dadc3b22d4cadbbf398b7a668531 /risc-v/riscv_extras.lem | |
| parent | 69dbe323ef6a8195465e2662fd447e1853e40866 (diff) | |
added RISC-V strong-acquire/release
Diffstat (limited to 'risc-v/riscv_extras.lem')
| -rw-r--r-- | risc-v/riscv_extras.lem | 29 |
1 files changed, 15 insertions, 14 deletions
diff --git a/risc-v/riscv_extras.lem b/risc-v/riscv_extras.lem index 62a7bb91..280095e5 100644 --- a/risc-v/riscv_extras.lem +++ b/risc-v/riscv_extras.lem @@ -34,8 +34,11 @@ let memory_parameter_transformer_option_address _mode v = let read_memory_functions : memory_reads = [ ("MEMr", (MR Read_plain memory_parameter_transformer)); ("MEMr_acquire", (MR Read_RISCV_acquire memory_parameter_transformer)); + ("MEMr_strong_acquire", (MR Read_RISCV_strong_acquire memory_parameter_transformer)); ("MEMr_reserved", (MR Read_RISCV_reserved memory_parameter_transformer)); ("MEMr_reserved_acquire", (MR Read_RISCV_reserved_acquire memory_parameter_transformer)); + ("MEMr_reserved_strong_acquire", + (MR Read_RISCV_reserved_acquire memory_parameter_transformer)); ] let memory_writes : memory_writes = @@ -44,25 +47,23 @@ let memory_writes : memory_writes = let memory_eas : memory_write_eas = [ ("MEMea", (MEA Write_plain memory_parameter_transformer)); ("MEMea_release", (MEA Write_RISCV_release memory_parameter_transformer)); + ("MEMea_strong_release", (MEA Write_RISCV_strong_release memory_parameter_transformer)); ("MEMea_conditional", (MEA Write_RISCV_conditional memory_parameter_transformer)); ("MEMea_conditional_release", (MEA Write_RISCV_conditional_release memory_parameter_transformer)); + ("MEMea_conditional_strong_release", + (MEA Write_RISCV_conditional_strong_release + memory_parameter_transformer)); ] let memory_vals : memory_write_vals = - [ ("MEMval", (MV memory_parameter_transformer_option_address Nothing)); - ("MEMval_release", (MV memory_parameter_transformer_option_address Nothing)); - ("MEMval_conditional", (MV memory_parameter_transformer_option_address Nothing)); - (* (MV memory_parameter_transformer_option_address - (Just - (fun (IState interp context) b -> - let bit = Interp_ast.V_lit (L_aux (if b then L_one else L_zero) Interp_ast.Unknown) in - (IState (Interp.add_answer_to_stack interp bit) context))))); *) - ("MEMval_conditional_release", (MV memory_parameter_transformer_option_address Nothing)); - (* (MV memory_parameter_transformer_option_address - (Just - (fun (IState interp context) b -> - let bit = Interp_ast.V_lit (L_aux (if b then L_one else L_zero) Interp_ast.Unknown) in - (IState (Interp.add_answer_to_stack interp bit) context))))); *) + [ ("MEMval", (MV memory_parameter_transformer_option_address Nothing)); + ("MEMval_release", (MV memory_parameter_transformer_option_address Nothing)); + ("MEMval_strong_release", (MV memory_parameter_transformer_option_address Nothing)); + ("MEMval_conditional", (MV memory_parameter_transformer_option_address Nothing)); + ("MEMval_conditional_release",(MV memory_parameter_transformer_option_address Nothing)); + ("MEMval_conditional_strong_release", + (MV memory_parameter_transformer_option_address Nothing)); + ] let speculate_conditional_success : excl_res = |