![](https://csdnimg.cn/release/download_crawler_static/8454165/bg8.jpg)
Therefore, each collector can recognize a source node immediately by checking if its srcnt field is
positive. We define:
R1(x) ≡ (∃z: srcnt[z] > 0: z
∗
−→ x),
and we have R(x) ⇒ R1(x). We do not apply other reference counting to the nodes, since manipulating
reference counters is slow and may incur expensive overhead with every duplication and deletion of
the pointers.
The main difficulty with tracing the memory graph is that the memory structure can dynamically
change during GC. In order to solve this problem, we need some coordination between mutators and
collectors to take the view of the memory graph, on which all collectors work. To avoid possible
interference between mutators and collectors (we will explain this later), the updates of the field
srcnt of the node in UnProtect, upon deletion from the roots set, is postponed until the end of GC.
We use the field freecnt to count the postponed decrementings of srcnt. The fields ari and father
contain the number of children a node has at the beginning of GC and the parent node of a node in
a tree traversed from a source node by collectors, respectively.
Moreover, since more than one process may participate in GC and they may operate concurrently
with mutators, we need to avoid interference from delayed processes. We use a shared variable shRnd
to hold the round number of the current GC, together with an additional field round in the record
of a node. The private variable rnd is a private copy of the shared variable shRnd. A process p
participates in the current round of GC if and only if rnd
p
= shRnd. We introduce the global private
variable toBeC to transfer information about checked nodes between internal calls. There is also a
local private variable toBeD.
3.2 Algorithm
In this section, we give a higher-level implementation for the collectors and the mutators. Since
procedure calls only modify private control data, procedure headers are not always labeled themselves,
but their bodies usually have numbered atomic statements. The labels are chosen identical to the
labels in the PVS code, and are therefore not completely consecutive.
Brackets J K and the actions between braces { } and parenthesis L M can be ignored in the imple-
mentation. They only serve in the proof of correctness. We will explain this in section 4.
3.2.1 Collectors
Our garbage collectors are encoded in the procedure GCollect as shown in Fig. 3. It is comprised of
three phases: (1) paint all black nodes grey while recording the current memory structure, (2) paint
all grey nodes reachable from the source nodes back to black after traversing the memory graph, and
(3) reclaim all garbage by painting all remaining grey nodes white. The transitions between the colors
are shown in Fig. 4.
Processes first let rnd get the current value of shRnd (this is the only action that updates the private
variable rnd) to prepare for participating in this round of GC. A new round of GC is started when
the fastest process reaches line 101 with rnd
self
= shRnd holding in the precondition. It is proved by
means of invariants that before a new round of GC is started, all earlier rounds of GC have completed:
∀x: 1 . . . N: round[x] = shRnd ∧ color[x] 6= grey.
In order to prevent some process from doing useless or even harmful work, every modification on a
node in each phase is protected by a guard, which can force a process (in particular, a process with
rnd
self
6= shRnd) to abandon its delayed operation.
In the first phase, from label 101 to label 108, processes try to update field round, paint black nodes
grey and record the present memory structure using fields ari and father. The processes only need
to paint the black nodes grey since the white nodes can not be garbage.
8