diff options
| author | Shaked Flur | 2017-08-31 15:08:10 +0100 |
|---|---|---|
| committer | Shaked Flur | 2017-08-31 15:08:10 +0100 |
| commit | 07fad742df72ff6e7bfb948c1c353a2cf12f5e28 (patch) | |
| tree | fbe53846d5fb7a3d3713545c6cd28db0c453a9a0 /risc-v/riscv_extras.lem | |
| parent | d9e3c14533806986f7c6ce843148cf1973f9711b (diff) | |
added RISC-V AMOs
Diffstat (limited to 'risc-v/riscv_extras.lem')
| -rw-r--r-- | risc-v/riscv_extras.lem | 19 |
1 files changed, 13 insertions, 6 deletions
diff --git a/risc-v/riscv_extras.lem b/risc-v/riscv_extras.lem index 59e3cd4a..62a7bb91 100644 --- a/risc-v/riscv_extras.lem +++ b/risc-v/riscv_extras.lem @@ -51,20 +51,27 @@ let memory_eas : memory_write_eas = 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 + ("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 + (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))))); + (IState (Interp.add_answer_to_stack interp bit) context))))); *) ] +let speculate_conditional_success : excl_res = + let f = fun (IState interp context) b -> + let bool_res = 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 bool_res) context + in + Just ("speculate_conditional_success", (ER (Just f))) + let barrier_functions = [ ("MEM_fence_rw_rw", Barrier_RISCV_rw_rw); ("MEM_fence_r_rw", Barrier_RISCV_r_rw); |