• Home
  • Raw
  • Download

Lines Matching +full:lock +full:- +full:state

5 This document describes implementation details of new-style "graph" data
13 Note that the intent of this document is to describe the current state of
22 ------------
31 no longer relevant. With the introduction of kfuncs, kptrs, and the any-context
35 Two such data structures - linked_list and rbtree - have many verification
44 ------------
47 helper functions - either standard map API helpers like ``bpf_map_update_elem``
48 or map-specific helpers. The new-style graph data structures instead use kfuncs
57 -------
59 The new-style data structures are intrusive and are defined similarly to their
62 .. code-block:: c
74 which also contains a ``bpf_spin_lock`` - in the above example both global
75 variables are placed in a single-value arraymap. The verifier considers this
77 the same map_value and will enforce that the correct lock is held when
78 verifying BPF programs that manipulate the tree. Since this lock checking
81 Non-owning references
82 ---------------------
88 .. code-block:: c
92 bpf_spin_lock(&lock);
96 bpf_spin_unlock(&lock);
102 The BPF program must pass off ownership before exiting - either via
120 .. code-block:: c
125 bpf_spin_lock(&lock);
128 x = n->data;
129 n->data = 42;
131 bpf_spin_unlock(&lock);
133 Both the read from and write to ``n->data`` would be rejected. The verifier
147 or removing, if we're in the critical section bounded by that lock, we know
153 The verifier considers such a reference a *non-owning reference*. The ref
172 *non-owning reference*
180 non-owning ref existence (see explanation below)
184 From verifier's perspective non-owning references can only exist
186 can do arbitrary operations on the data structure like removing and ``free``-ing
187 via bpf_obj_drop. A non-owning ref to some chunk of memory that was remove'd,
191 To prevent this logic violation all non-owning references are invalidated by the
193 not page fault" property of non-owning references. So if the verifier hasn't
194 invalidated a non-owning ref, accessing it will not page fault.
197 if there's a valid non-owning ref, we must be in a critical section, and can
198 conclude that the ref's memory hasn't been dropped-and- ``free``'d or
199 dropped-and-reused.
201 Any reference to a node that is in an rbtree _must_ be non-owning, since
206 allows the verifier to prevent such a state from being valid by simply checking
212 .. code-block:: c
217 bpf_spin_lock(&lock);
225 bpf_spin_unlock(&lock);
230 Assume the tree is empty before this program runs. If we track verifier state
235 2) n is a non-owning reference, it's been added to the tree
237 3) n and m are non-owning references, they both point to the same node
239 4) o is an owning reference, n and m non-owning, all point to same node
241 5) o and p are owning, n and m non-owning, all point to the same node
243 6) a double-free has occurred, since o and p point to same node and o was
246 States 4 and 5 violate our "nice property", as there are non-owning refs to
248 has already been removed as a result of this violation. State 6 is a dangerous
249 double-free.
251 At a minimum we should prevent state 6 from being possible. If we can't also
252 prevent state 5 then we must abandon our "nice property" and check whether a
255 We prevent both by generalizing the "invalidate non-owning references" behavior
265 May result in a state where some other non-owning reference points to the same
266 node. So ``remove``-type kfuncs must be considered a non-owning reference