5. Principles of Model Checking. Baier_ Joost (2008) (811406), страница 55
Текст из файла (страница 55)
Then, for any path π ∈ P aths(TS) either π |= fair ∧ ϕ orπ |= ¬fair . Thus, π |= (fair → ϕ), and consequently TS |= (fair → ϕ).⇐: by a similar reasoning.Example 5.31.On-The-Fly Garbage CollectionAn important characteristic of pointer-manipulating programs is that certain parts of thedynamically changing data structure, such as a list or a tree, may become inaccessible.That is to say, this part of the data structure is not “reachable” by dereferencing oneof the program variables. In order to be able to recycle these inaccessible memory cells,so-called garbage collecting algorithms are employed.
These algorithms are key parts ofoperating systems, and play a major role in compilers. In this example, we focus on onthe-fly garbage collection algorithms. These algorithms attempt to identify and recycleinaccessible memory cells concurrently with the running programs that may manipulatethe dynamically changing data structure. Typical requirements for such garbage collectionalgorithms areSafety: An accessible (i.e., reachable) memory cell is never collected.Liveness: Any unreachable storage cell is eventually collected.The memory cells. The memory is considered to consist of a fixed number N of memorycells. The number of memory cells is static, i.e., the dynamic allocation and deallocationof cells (as in the C-statement malloc) is not considered.
The memory cells are organizedin a directed graph, whose structure may change during the computation; this happens,e.g., when carrying out an assignment v := w where v and w point to a memory cell. Forthe sake of simplicity, it is assumed that each cell (= vertex) has at most one pointer (=edge) to another cell. Let son(i) denote the immediate successor of cell i.
Cells that do nothave an outgoing reference are equipped with a self-reference. Thus, each cell has exactlyone outgoing edge in the graph representation. Vertices are numbered. There is a fixed setof root vertices. Root cells are never considered as garbage. A memory cell is reachable ifit is reachable in the graph from a root vertex. Cells that are not reachable from a rootvertex are garbage cells. The memory is partitioned into three fragments: the accessiblecells (i.e., cells that are reachable by the running processes), the free cells (i.e., cells thatare unused and that can be assigned to running processes), and the unreachable cells. Asfor the garbage collection algorithm, it is only of importance which cells are unreachable.The distinction between free and accessible cells is of no importance, and will be neglectedin the remainder.266Linear Temporal LogicModeling the garbage collector.
The entire system is modeled as the parallel compositionof the garbage collector (process Collector), and a process that models the behaviour ofthe running processes manipulating the shared data structure. Thus:Mutator CollectorFor simplicity, we abstain from a detailed transition system representation and describe themutator and the collector by pseudocode algorithms. As the garbage collecting algorithmshould work correctly for any arbitrary set of concurrently running processes, the mutatoris modeled by means of a single process that can nondeterministically choose two arbitraryreachable cells i and k and change the current reference i → j into i → k.
This correspondsto the assignment “son(i) := k”. Note that if i was the only cell pointing to j, then afterthe assignment son(i) := k, the memory cell j has become garbage.Algorithm 9 Mutator and garbage collector (naive version)(* mutator *)while true doNondeterministically choose two reachable nodes i and k;son(i) := kod(* garbage collector *)while true dolabel all reachable cells;(* e.g., by depth-first search *)for all cells i doif i is not labeled then collect iodadd the collected cells to the list of free memory cellsodNow let us consider the garbage collector. A naive technique could be based on a DFSor BFS which labels cells and, subsequently, collects all unlabeled cells as garbage (seeAlgorithm 9).
The collected cells are added to the list of free memory cells, and thusare turned into reachable cells. This simple idea works correctly when the actions of themutator are not interlocked with those of the garbage collector. As an on-the-fly algorithm,however, this naive idea fails due to the possible interleavings between the mutator and thecollector. This is illustrated in Figure 5.12 where six memory configurations are depicted.Circles denote memory cells and edges represent the pointer structure. Nonshaded cellsare not visited, gray ones are visited, and cells with a thick border have been completelyprocessed. Due to the changes made by the mutator during the garbage collection phase,one of the memory cells remains unlabeled although it is accessible.
The collector wouldnow collect the unlabeled but accessible cell.Linear Temporal Logic267CollectorCollectorMutatorCollectorMutatorFigure 5.12: Failure of the naive garbage collector.An alternative is to use a labeling algorithm that successively passes through all cells andlabels their sons if the appropriate cell is labeled itself. Initially, only root cells are labeled.This technique is iterated as long as the number of labeled cells does not change anymore.The auxiliary variables M and Mold are used to this purpose.
M counts the number oflabeled cells in the current stage of labeling. Mold stands for the number of labeled cellsin the previous stage of labeling. Additionally, the mutator supports the labeling processby labeling cell k as soon as a reference is redirected to k (see Algorithm 10). It is notdifficult to show that the participation of the mutator is necessary to obtain a correctgarbage collection algorithm. If it does not participate, there can always be found someinterference pattern between the mutator and the collector such that reachable cells aremade inaccessible by the mutator, causing a flaw in the garbage collection.
Figure 5.13demonstrates the functioning of the collector for four linearly linked reachable cells, whereit is assumed that the labeling steps of the collector are not interrupted by the mutator.The shading represents the labeling by the collector. The thick border of a node indicatesthat this node was considered in the for loop. Thus, in the last step, all four nodes wereprocessed in the for loop.
Therefore, the result of the first iteration is Mold = 1 (numberof root cells) and M = 3, since exactly three cells were labeled. The labels arising at theend of the subsequent iterations are indicated in Figure 5.14.Figure 5.15 shows an example that indicates that the mutator has to label cells, as otherwise it cannot be ensured that the collector identifies all reachable cells. The leftmostfigure indicates the starting memory configuration.
The situation after the collector haslabeled the root cell and has processed the top left node in the FOR loop is depicted in268Linear Temporal LogicAlgorithm 10 Ben Ari’s on-the-fly garbage collection algorithm(* mutator *)while true dolet i and k be reachable memory cells;label k;son(i) := kod(* garbage collector *)while true dolabel all root cells;M := number of root cells;repeatMold := M ;for all node i doif i is labeled thenif son(i) is unlabeled then label son(i); M := M +1; fifioduntil M = Mold ;for all cell i doif i is labeled then delete label for cell ielse collect cell ifiodadd the collected cells to the list of free cellsod(* cell i is garbage *)Linear Temporal Logic269111111444444333333222222Figure 5.13: Example of Ben Ari’s on-the-fly garbage collector (one iteration).11441Mold = 1M =341Mold = 3M =44Mold = M = 433332222Figure 5.14: Example of Ben-Ari’s on-the-fly garbage collector (all iterations).the next figure.
The third and fourth figures show a possible modification of the pointerstructure by the mutator. The collector then would investigate the upper cell on the rightand label it. Since this cell does not have an unlabeled successor, the first round of thecollector is finished. As the obtained memory configuration is symmetric to the initial one,the whole procedure might be repeated, which leads to the initial configuration of Figure5.15. In the second round, the collector also just labels the two upper cells. Since thenumber of labeled cells has not increased and assuming that the mutator does not labelthe lower cell, this cell would be wrongly regarded as garbage (and thus be collected).The examples illustrate the functioning of the algorithm but are by no means meant asproof of correctness.
Due to the enormous size of the state space and the extremely highdegree of nondeterminism, the analysis of the garbage collection algorithm is extremelydifficult. Note that the states of the transition system, which results from the parallelcomposition of mutator and collector, consist of control components plus a representationof the current labels and of another component that gives information about the current270Linear Temporal LogicCollectorMutatorMutatorFigure 5.15: Labeling memory cells by the mutator is necessary.memory configuration. For N nodes, there exist 2N possible labels and N N possiblegraphs.
The high degree of nondeterminism results from the mutator that can change anarbitrary pointer. It is not useful to restrict the mutator (and thus reducing the degree ofnondeterminism), since this would impose restrictions on the applicability of the garbagecollecting algorithm.To conclude, we will formalize the requirements on the concurrent garbage collectionalgorithm. To that end, let atomic proposition collect(i) hold for cell i in a state if andonly if cell i has been collected in that state. Similarly, accessible(i) holds in those statesin which cell i is reachable from a root cell. Given these atomic propositions, the safetyproperty “an accessible memory cell is never collected” can be specified as( collect(i) → ¬accessible(i) ).0<iNThe liveness property “any unreachable storage cell is eventually collected” is describedas LTL formula( ¬accessible(i) → ♦collect(i) ).0<iNIt turns out that Ben Ari’s concurrent garbage collection algorithm satisfies the safetyproperty, but refutes the liveness property.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
