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