diff --git a/lib/concurrency_interface/translation.sail b/lib/concurrency_interface/translation.sail
new file mode 100644
index 000000000..276f9536e
--- /dev/null
+++ b/lib/concurrency_interface/translation.sail
@@ -0,0 +1,89 @@
+/*==========================================================================*/
+/* Sail */
+/* */
+/* Sail and the Sail architecture models here, comprising all files and */
+/* directories except the ASL-derived Sail code in the aarch64 directory, */
+/* are subject to the BSD two-clause licence below. */
+/* */
+/* The ASL derived parts of the ARMv8.3 specification in */
+/* aarch64/no_vector and aarch64/full are copyright ARM Ltd. */
+/* */
+/* Copyright (c) 2013-2024 */
+/* Kathyrn Gray */
+/* Shaked Flur */
+/* Stephen Kell */
+/* Gabriel Kerneis */
+/* Robert Norton-Wright */
+/* Christopher Pulte */
+/* Peter Sewell */
+/* Alasdair Armstrong */
+/* Brian Campbell */
+/* Thomas Bauereiss */
+/* Anthony Fox */
+/* Jon French */
+/* Dominic Mulligan */
+/* Stephen Kell */
+/* Mark Wassell */
+/* Alastair Reid (Arm Ltd) */
+/* */
+/* All rights reserved. */
+/* */
+/* This work was partially supported by EPSRC grant EP/K008528/1 REMS: Rigorous */
+/* Engineering for Mainstream Systems, an ARM iCASE award, EPSRC IAA */
+/* KTF funding, and donations from Arm. This project has received */
+/* funding from the European Research Council (ERC) under the European */
+/* Union’s Horizon 2020 research and innovation programme (grant */
+/* agreement No 789108, ELVER). */
+/* */
+/* This software was developed by SRI International and the University of */
+/* Cambridge Computer Laboratory (Department of Computer Science and */
+/* Technology) under DARPA/AFRL contracts FA8650-18-C-7809 ("CIFV") */
+/* and FA8750-10-C-0237 ("CTSRD"). */
+/* */
+/* Redistribution and use in source and binary forms, with or without */
+/* modification, are permitted provided that the following conditions */
+/* are met: */
+/* 1. Redistributions of source code must retain the above copyright */
+/* notice, this list of conditions and the following disclaimer. */
+/* 2. Redistributions in binary form must reproduce the above copyright */
+/* notice, this list of conditions and the following disclaimer in */
+/* the documentation and/or other materials provided with the */
+/* distribution. */
+/* */
+/* THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS'' */
+/* AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED */
+/* TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A */
+/* PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR OR */
+/* CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, */
+/* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT */
+/* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF */
+/* USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND */
+/* ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, */
+/* OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT */
+/* OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF */
+/* SUCH DAMAGE. */
+/*==========================================================================*/
+
+$sail_internal
+
+$ifndef _CONCURRENCY_INTERFACE_TRANSLATION
+$define _CONCURRENCY_INTERFACE_TRANSLATION
+
+$include
+
+outcome sail_translation_start : 'trans_start -> unit
+with
+ 'trans_start : Type
+= {
+ impl emulator(_) = ()
+}
+
+outcome sail_translation_end : 'trans_end -> unit
+with
+ 'trans_end : Type
+= {
+ impl emulator(_) = ()
+}
+
+$endif
diff --git a/src/lib/monad_params.ml b/src/lib/monad_params.ml
index 36e1fdb13..d07113869 100644
--- a/src/lib/monad_params.ml
+++ b/src/lib/monad_params.ml
@@ -78,6 +78,8 @@ type parameters = {
pa_type : typ;
tlbi_type : typ;
translation_summary_type : typ;
+ trans_start_type : typ;
+ trans_end_type : typ;
arch_ak_type : typ;
}
@@ -121,6 +123,8 @@ let find_monad_parameters type_env =
let cache_op_type = extract_arg_typ "sail_cache_op" in
let fault_type = extract_arg_typ "sail_take_exception" in
let tlbi_type = extract_arg_typ "sail_tlbi" in
+ let trans_start_type = extract_arg_typ "sail_translation_start" in
+ let trans_end_type = extract_arg_typ "sail_translation_end" in
Some
{
abort_type;
@@ -130,5 +134,7 @@ let find_monad_parameters type_env =
pa_type;
tlbi_type;
translation_summary_type;
+ trans_start_type;
+ trans_end_type;
arch_ak_type;
}
diff --git a/src/sail_coq_backend/pretty_print_coq.ml b/src/sail_coq_backend/pretty_print_coq.ml
index 4420400df..e53962174 100644
--- a/src/sail_coq_backend/pretty_print_coq.ml
+++ b/src/sail_coq_backend/pretty_print_coq.ml
@@ -3630,6 +3630,8 @@ let pp_ast_coq (types_file, types_modules) (defs_file, defs_modules) type_defs_m
string " Definition pa_countable : Countable pa := _.";*)
string " Definition arch_ak := " ^^ pp_typ params.arch_ak_type ^^ string ".";
string " Definition translation := " ^^ pp_typ params.translation_summary_type ^^ string ".";
+ string " Definition trans_start := " ^^ pp_typ params.trans_start_type ^^ string ".";
+ string " Definition trans_end := " ^^ pp_typ params.trans_end_type ^^ string ".";
string " Definition abort := " ^^ pp_typ params.abort_type ^^ string ".";
string " Definition barrier := " ^^ pp_typ params.barrier_type ^^ string ".";
string " Definition cache_op := " ^^ pp_typ params.cache_op_type ^^ string ".";
diff --git a/src/sail_lem_backend/pretty_print_lem.ml b/src/sail_lem_backend/pretty_print_lem.ml
index 969382246..9a724ddf2 100644
--- a/src/sail_lem_backend/pretty_print_lem.ml
+++ b/src/sail_lem_backend/pretty_print_lem.ml
@@ -1831,6 +1831,8 @@ let doc_ast_lem out_filename split_files base_imports extra_imports effect_info
params.pa_type;
params.tlbi_type;
params.translation_summary_type;
+ params.trans_start_type;
+ params.trans_end_type;
params.arch_ak_type;
]
in