# HG changeset patch
# User Paul Boddie <paul@boddie.org.uk>
# Date 1664636601 -7200
# Node ID 753474408f12e0ea60c00cf4cd3bb71be928788b
# Parent  2ecda157686f026bdef962894b41d529bc8032c3
Added some remarks about the perceived nature of the opcode type problem.

diff -r 2ecda157686f -r 753474408f12 libsystypes/idl/dataspace.idl
--- a/libsystypes/idl/dataspace.idl	Sat Oct 01 16:58:16 2022 +0200
+++ b/libsystypes/idl/dataspace.idl	Sat Oct 01 17:03:21 2022 +0200
@@ -7,7 +7,15 @@
 interface Dataspace
 {
   /* Map memory within a dataspace.
-     NOTE: Using opcode_type to work around L4Re dataspace IPC issues. */
+     NOTE: Using opcode_type to work around L4Re dataspace IPC issues. In
+           principle, this workaround is unnecessary for AMD64 and MIPS32
+           because even in the latter case, the opcode will be followed by the
+           64-bit offset aligned to a 64-bit boundary. Here, both the structure
+           used to interpret the message and the L4Re RPC framework agree.
+           However, on IA32, the "alignment requirement" of the 64-bit offset is
+           actually only 32 bits, meaning that the offset structure member will
+           immediately follow the opcode, but the L4Re RPC framework seems to
+           observe a different alignment regime. */
 
   [opcode(0),opcode_type(l4_uint64_t)] void map(in offset_t offset, in map_address_t hot_spot,
                        in map_flags_t flags, out fpage region);