detcore_model/
futex.rs

1/*
2 * Copyright (c) Meta Platforms, Inc. and affiliates.
3 * All rights reserved.
4 *
5 * This source code is licensed under the BSD-style license found in the
6 * LICENSE file in the root directory of this source tree.
7 */
8
9use serde::Deserialize;
10use serde::Serialize;
11
12use crate::fd::OpenFileId;
13use crate::pid::DetTid;
14
15/// Identity of a Linux memory address space (`mm_struct`).
16#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash, Serialize, Deserialize)]
17pub struct MmId {
18    creator: DetTid,
19    generation: u64,
20}
21
22impl MmId {
23    /// Deterministic task that created this model address-space incarnation.
24    /// This is an equality binding, not kernel memory-management attestation.
25    pub const fn creator(self) -> DetTid {
26        self.creator
27    }
28
29    /// Exact monotonic model exec generation, including initial generation zero.
30    pub const fn generation(self) -> u64 {
31        self.generation
32    }
33
34    /// Create the initial address space owned by a task.
35    pub const fn initial(creator: DetTid) -> Self {
36        Self {
37            creator,
38            generation: 0,
39        }
40    }
41
42    /// Inherit an address space for `CLONE_VM`, otherwise create a fresh identity.
43    pub const fn for_clone(parent: Self, child: DetTid, shares_vm: bool) -> Self {
44        if shares_vm {
45            parent
46        } else {
47            Self::initial(child)
48        }
49    }
50
51    /// Create the replacement address space installed by exec.
52    pub fn for_exec(self, creator: DetTid) -> Self {
53        Self {
54            creator,
55            // Exec generations must remain monotonic even when Linux changes a
56            // non-leader caller's TID to the process leader's TID.
57            generation: self.generation + 1,
58        }
59    }
60}
61
62/// Identity of an object that backs a process-shared memory mapping.
63#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash, Serialize, Deserialize)]
64pub enum SharedMemoryObjectId {
65    /// Anonymous shared mapping, identified by its deterministic allocation.
66    Anonymous {
67        /// Address space in which the mapping was created.
68        origin: MmId,
69        /// Per-address-space mapping sequence.
70        sequence: u64,
71    },
72    /// File-backed shared mapping.
73    File {
74        /// Device containing the file.
75        device: u64,
76        /// Inode of the file.
77        inode: u64,
78    },
79    /// Open-file-description fallback used when inode metadata is unavailable.
80    OpenFile { id: OpenFileId },
81}
82
83/// Identity of a futex word.
84#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash, Serialize, Deserialize)]
85pub enum FutexID {
86    /// Process-private futex, keyed by its address space and virtual address.
87    Private { mm: MmId, address: usize },
88    /// Process-shared futex, keyed by its backing object and byte offset.
89    Shared {
90        object: SharedMemoryObjectId,
91        offset: u64,
92    },
93}
94
95impl FutexID {
96    /// Create a private futex key.
97    pub const fn private(mm: MmId, address: usize) -> Self {
98        Self::Private { mm, address }
99    }
100
101    /// Create a process-shared futex key.
102    pub const fn shared(object: SharedMemoryObjectId, offset: u64) -> Self {
103        Self::Shared { object, offset }
104    }
105}
106
107#[cfg(test)]
108mod tests {
109    use super::*;
110
111    #[test]
112    fn clone_vm_controls_private_futex_aliasing() {
113        let parent = MmId::initial(DetTid::from_raw(10));
114        let child = DetTid::from_raw(11);
115
116        assert_eq!(
117            FutexID::private(parent, 0x1000),
118            FutexID::private(MmId::for_clone(parent, child, true), 0x1000),
119            "CLONE_VM tasks should use the same private futex key"
120        );
121        assert_ne!(
122            FutexID::private(parent, 0x1000),
123            FutexID::private(MmId::for_clone(parent, child, false), 0x1000),
124            "a copied address space should not alias the parent's private futex"
125        );
126        assert_ne!(
127            FutexID::private(parent, 0x1000),
128            FutexID::private(parent.for_exec(DetTid::from_raw(10)), 0x1000),
129            "exec should replace the private futex namespace"
130        );
131    }
132
133    #[test]
134    fn exec_generation_never_repeats_when_caller_identity_changes() {
135        let leader = DetTid::from_raw(10);
136        let worker = DetTid::from_raw(11);
137        let initial = MmId::initial(leader);
138        let worker_exec = initial.for_exec(worker);
139        let leader_exec = worker_exec.for_exec(leader);
140
141        assert_ne!(worker_exec, initial);
142        assert_ne!(leader_exec, initial);
143        assert_ne!(leader_exec, worker_exec);
144    }
145
146    #[test]
147    fn shared_futexes_alias_by_object_and_offset() {
148        let object = SharedMemoryObjectId::File {
149            device: 10,
150            inode: 20,
151        };
152        assert_eq!(
153            FutexID::shared(object, 64),
154            FutexID::shared(object, 64),
155            "virtual-address aliases of one backing offset must share a key"
156        );
157        assert_ne!(
158            FutexID::shared(object, 64),
159            FutexID::shared(object, 68),
160            "different words in one backing object need distinct keys"
161        );
162        assert_ne!(
163            FutexID::shared(object, 64),
164            FutexID::private(MmId::initial(DetTid::from_raw(10)), 64),
165            "private and shared namespaces must remain distinct"
166        );
167    }
168}
detcore_model/futex.rs

detcore_model/
futex.rs
