| |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Using Promela and Spin to verify parallel algorithmsValidating Parallel AlgorithmsParallel algorithms can be hard to write, and even harder to debug. Testing, though essential, is insufficient, as fatal race conditions can have extremely low probabilities of occurrence. Proofs of correctness can be valuable, but in the end are just as prone to human error as is the original algorithm.It would be very helpful to have a tool that could somehow locate all race conditions. Such a tool in fact exists in the form of the language Promela and its compiler Spin. What are Promela and Spin?Promela is a language designed to help verify protocols, but which can also be used to verify small parallel algorithms. You recode your algorithm and correctness constraints in the C-like language Promela, and then use Spin to translate it into a C program that you can compile and run. The resulting program conducts a full state-space search of your algorithm, either verifying or finding counter-examples for assertions that you can include in your Promela program.This full-state search can be extremely powerful, but can also be a two-edged sword. If your algorithm is too complex or your Promela implementation is careless, there might be more states than fit in memory. Furthermore, even given sufficient memory, the state-space search might well run for longer than the expected lifetime of the universe. Therefore, use this tool for compact but complex parallel algorithms. Attempts to naively apply it to even moderate-scale algorithms (let alone the full Linux kernel) will end badly. Promela and Spin may be downloaded from here. The above site also gives links to Gerard Holzmann's excellent book on Promela and Spin, as well as online references starting here. The remainder of this article describes how to use Promela to debug parallel algorithms, starting with simple examples and progressing to more complex uses.
Promela Example: Non-Atomic IncrementThe following example demonstrates the textbook race condition resulting from non-atomic increment:
1 #define NUMPROCS 2
2
3 byte counter = 0;
4 byte progress[NUMPROCS];
5
6 proctype incrementer(byte me)
7 {
8 int temp;
9
10 temp = counter;
11 counter = temp + 1;
12 progress[me] = 1;
13 }
14
15 init {
16 int i = 0;
17 int sum = 0;
18
19 atomic {
20 i = 0;
21 do
22 :: i < NUMPROCS ->
23 progress[i] = 0;
24 run incrementer(i);
25 i++
26 :: i >= NUMPROCS -> break
27 od;
28 }
29 atomic {
30 i = 0;
31 sum = 0;
32 do
33 :: i < NUMPROCS ->
34 sum = sum + progress[i];
35 i++
36 :: i >= NUMPROCS -> break
37 od;
38 assert(sum < NUMPROCS || counter == NUMPROCS)
39 }
40 }
Line 1 defines the number of processes to run (we will vary this
to see the effect on state space), line 3 defines the counter,
and line 4 is used to implement the assertion that appears on
lines 29-39.
Lines 6-13 define a process that increments the counter non-atomically. The argument "me" is the process number, set by the initialization block later in the code. Because simple Promela statements are each assumed atomic, we must break the increment into the two statements on lines 10-11. The assignment on line 12 marks the process's completion. Because the Spin system will fully search the state space, including all possible sequences of states, there is no need for the loop that would be used for conventional testing. Lines 15-40 are the initialization block, which is executed first. Lines 19-28 actually do the initialization, while lines 29-39 perform the assertion. Both are atomic blocks in order to avoid unnecessarily increasing the state space: because they are not part of the algorithm proper, we loose no validation coverage by making them atomic. The do-od construct on lines 21-27 implements a Promela loop, which can be thought of as a C "for (;;)" loop containing a "switch" statement that allows expressions in case labels. The condition blocks (prefixed by "::") are scanned non-deterministically, though in this case only one of the conditions can possibly hold at a given time. The first block of the do-od from lines 22-25 initializes the i-th incrementer's progress cell, runs the i-th incrementer's process, and then increments the variable "i". The second block of the do-od on line 26 exits the loop once these processes have been started. The atomic block on lines 29-39 also contains a similar do-od loop that sums up the progress counters. The assert() statement on line 38 verifies that if all processes have been completed, then all counts have been correctly recorded. You can build and run this program as follows:
spin -a increment.spin # Translate the model to C
cc -DSAFETY -o pan pan.c # Compile the model
./pan # Run the model
This will produce output as follows:
pan: assertion violated ((sum<2)||(counter==2)) (at depth 20)
pan: wrote increment.spin.trail
(Spin Version 4.2.5 -- 2 April 2005)
Warning: Search not completed
+ Partial Order Reduction
Full statespace search for:
never claim - (none specified)
assertion violations +
cycle checks - (disabled by -DSAFETY)
invalid end states +
State-vector 40 byte, depth reached 22, errors: 1
45 states, stored
13 states, matched
58 transitions (= stored+matched)
51 atomic steps
hash conflicts: 0 (resolved)
2.622 memory usage (Mbyte)
The first line tells us that our assertion was violated (as expected
given the non-atomic increment!).
The second line that a "trail" file was written describing how the
assertion was violated.
The "Warning" line reiterates that all was not well with our model.
The second paragraph describes the type of state-search being carried out,
in this case for assertion violations and invalid end states.
The third paragraph gives state-size statistics: this small model had only
45 states.
The final line shows memory usage.
The "trail" file may be rendered human-readable as follows:
spin -t -p increment.spin
This gives the following output:
Starting :init: with pid 0
1: proc 0 (:init:) line 20 "increment.spin" (state 1) [i = 0]
2: proc 0 (:init:) line 22 "increment.spin" (state 2) [((i<2))]
2: proc 0 (:init:) line 23 "increment.spin" (state 3) [progress[i] = 0]
Starting incrementer with pid 1
3: proc 0 (:init:) line 24 "increment.spin" (state 4) [(run incrementer(i))]
3: proc 0 (:init:) line 25 "increment.spin" (state 5) [i = (i+1)]
4: proc 0 (:init:) line 22 "increment.spin" (state 2) [((i<2))]
4: proc 0 (:init:) line 23 "increment.spin" (state 3) [progress[i] = 0]
Starting incrementer with pid 2
5: proc 0 (:init:) line 24 "increment.spin" (state 4) [(run incrementer(i))]
5: proc 0 (:init:) line 25 "increment.spin" (state 5) [i = (i+1)]
6: proc 0 (:init:) line 26 "increment.spin" (state 6) [((i>=2))]
7: proc 0 (:init:) line 21 "increment.spin" (state 10) [break]
8: proc 2 (incrementer) line 10 "increment.spin" (state 1) [temp = counter]
9: proc 1 (incrementer) line 10 "increment.spin" (state 1) [temp = counter]
10: proc 2 (incrementer) line 11 "increment.spin" (state 2) [counter = (temp+1)]
11: proc 2 (incrementer) line 12 "increment.spin" (state 3) [progress[me] = 1]
12: proc 2 terminates
13: proc 1 (incrementer) line 11 "increment.spin" (state 2) [counter = (temp+1)]
14: proc 1 (incrementer) line 12 "increment.spin" (state 3) [progress[me] = 1]
15: proc 1 terminates
16: proc 0 (:init:) line 30 "increment.spin" (state 12) [i = 0]
16: proc 0 (:init:) line 31 "increment.spin" (state 13) [sum = 0]
17: proc 0 (:init:) line 33 "increment.spin" (state 14) [((i<2))]
17: proc 0 (:init:) line 34 "increment.spin" (state 15) [sum = (sum+progress[i])]
17: proc 0 (:init:) line 35 "increment.spin" (state 16) [i = (i+1)]
18: proc 0 (:init:) line 33 "increment.spin" (state 14) [((i<2))]
18: proc 0 (:init:) line 34 "increment.spin" (state 15) [sum = (sum+progress[i])]
18: proc 0 (:init:) line 35 "increment.spin" (state 16) [i = (i+1)]
19: proc 0 (:init:) line 36 "increment.spin" (state 17) [((i>=2))]
20: proc 0 (:init:) line 32 "increment.spin" (state 21) [break]
spin: line 38 "increment.spin", Error: assertion violated
spin: text of failed assertion: assert(((sum<2)||(counter==2)))
21: proc 0 (:init:) line 38 "increment.spin" (state 22) [assert(((sum<2)||(counter==2)))]
spin: trail ends after 21 steps
#processes: 1
counter = 1
progress[0] = 1
progress[1] = 1
21: proc 0 (:init:) line 40 "increment.spin" (state 24) <valid end state>
3 processes created
As can be seen, the first portion of the init block created both
incrementer processes, both of which first fetched the counter,
then both incremented and stored it, losing a count.
The assertion then triggered, after which the global state is displayed.
Promela Example: Atomic IncrementIt is easy to fix this example by placing the body of the incrementer processes in an atomic blocks as follows:
1 proctype incrementer(byte me)
2 {
3 int temp;
4
5 atomic {
6 temp = counter;
7 counter = temp + 1;
8 }
9 progress[me] = 1;
10 }
One could also have simply replaced the pair of statements with
counter = counter + 1, because Promela statements are
atomic.
Either way, running this modified model gives us an error-free traversal
of the state space:
(Spin Version 4.2.5 -- 2 April 2005)
+ Partial Order Reduction
Full statespace search for:
never claim - (none specified)
assertion violations +
cycle checks - (disabled by -DSAFETY)
invalid end states +
State-vector 40 byte, depth reached 20, errors: 0
52 states, stored
21 states, matched
73 transitions (= stored+matched)
66 atomic steps
hash conflicts: 0 (resolved)
2.622 memory usage (Mbyte)
unreached in proctype incrementer
(0 of 5 states)
unreached in proctype :init:
(0 of 24 states)
Combinatorial ExplosionThe following table shows the number of states and memory consumed as a function of number of incrementers modeled (by redefining NUMPROCS):
Running unnecessarily large models is thus subtly discouraged, although 652MB is well within the limits of some of the more recent desktop and laptop machines. With this example under our belt, let's take a closer look at the commands used to analyze Promela models and then look at more elaborate examples.
How to Use PromelaGiven a source file "qrcu.spin", one can use the following commands: spin -a qrcu.spin Create a file pan.c that fully searches the state machine. cc -DSAFETY -o pan pan.c Compile the generated state-machine search. The "-DSAFETY" generates optimizations that are appropriate if you have only assertions (and perhaps "never" statements). If you have liveness, fairness, or forward-progress checks, you may need to compile without "-DSAFETY". If you leave off "-DSAFETY" when you could have used it, the program will let you know. ./pan This actually searches the state space. The number of states can reach into the tens of millions with very small state machines, so you will need a machine with large memory. For example, qrcu.spin with 3 readers and 2 updaters required 2.7GB of memory. spin -t -p qrcu.spin Given "trail" file output by a run that encountered an error, output the sequence of steps leading to that error.
Promela PeculiaritiesAlthough all computer languages have underlying similarities, Promela will provide some surprises to people used to coding in C.
Promela Coding TricksPromela was designed to analyze protocols, so using it on parallel programs is a bit abusive. The following tricks can help you to abuse Promela safely:
Promela Example: LockingSince locks are generally useful, spin_lock() and spin_unlock() macros are provided in lock.h, which may be included from multiple Promela models:
1 #define spin_lock(mutex) \
2 do \
3 :: 1 -> atomic { \
4 if \
5 :: mutex == 0 -> \
6 mutex = 1; \
7 break \
8 :: else -> skip \
9 fi \
10 } \
11 od
12
13 #define spin_unlock(mutex) \
14 mutex = 0
The spin_lock() macro contains an infinite do-od loop
spanning lines 2-11,
courtesy of the single guard expression of "1" on line 3.
The body of this loop is a single atomic block that contains
an if-fi statement.
The if-fi construct is similar to the do-od construct, except
that it takes a single pass rather than looping.
If the lock is not held on line 5, then line 6 acquires it and
line 7 breaks out of the enclosing do-od loop (and also exits
the atomic block).
On the other hand, if the lock is already held on line 8,
we do nothing ("skip"), and fall out of the if-fi and the
atomic block so as to take another pass through the outer
loop, repeating until the lock is available.
The spin_unlock() macro simply marks the lock as no longer held. Note that memory barriers are not needed because Promela assumes full ordering. In any given Promela state, all processes agree on both the current state and the order of state changes that caused us to arrive at the current state. This is analogous to the "sequentially consistent" memory model used by a few computer systems (such as MIPS and PA-RISC). As noted earlier, and as will be seen in a later example, weak memory ordering must be explicitly coded. These macros are tested by the following Promela code:
1 #include "lock.h"
2
3 #define N_LOCKERS 3
4
5 bit mutex = 0;
6 bit havelock[N_LOCKERS];
7 int sum;
8
9 proctype locker(byte me)
10 {
11 do
12 :: 1 ->
13 spin_lock(mutex);
14 havelock[me] = 1;
15 havelock[me] = 0;
16 spin_unlock(mutex)
17 od
18 }
19
20 init {
21 int i = 0;
22 int j;
23
24 end: do
25 :: i < N_LOCKERS ->
26 havelock[i] = 0;
27 run locker(i);
28 i++
29 :: i >= N_LOCKERS ->
30 sum = 0;
31 j = 0;
32 atomic {
33 do
34 :: j < N_LOCKERS ->
35 sum = sum + havelock[j];
36 j = j + 1
37 :: j >= N_LOCKERS ->
38 break
39 od
40 }
41 assert(sum <= 1);
42 break
43 od
44 }
This code is similar to that used to test the increments,
with the number of locking processes defined by the N_LOCKERS
macro definition on line 3.
The mutex itself is defined on line 5, an array to track the lock owner
on line 6, and line 7 is used by assertion
code to verify that only one process holds the lock.
The locker process is on lines 9-18, and simply loops forever acquiring the lock on line 13, claiming it on line 14, unclaiming it on line 15, and releasing it on line 16. The init block on lines 20-44 initializes the current locker's havelock array entry on line 26, starts the current locker on line 27, and advances to the next locker on line 28. Once all locker processes are spawned, the do-od loop moves to line 29, which checks the assertion. Lines 30 and 31 initialize the control variables, lines 32-40 atomically sum the havelock array entries, line 41 is the assertion, and line 42 exits the loop. We can run this model by placing the above two code fragments into files named "lock.h" and "lock.spin", respectively, and then running the following commands:
spin -a lock.spin
cc -DSAFETY -o pan pan.c
./pan
The output will look something like the following:
(Spin Version 4.2.5 -- 2 April 2005)
+ Partial Order Reduction
Full statespace search for:
never claim - (none specified)
assertion violations +
cycle checks - (disabled by -DSAFETY)
invalid end states +
State-vector 40 byte, depth reached 357, errors: 0
564 states, stored
929 states, matched
1493 transitions (= stored+matched)
368 atomic steps
hash conflicts: 0 (resolved)
2.622 memory usage (Mbyte)
unreached in proctype locker
line 18, state 20, "-end-"
(1 of 20 states)
unreached in proctype :init:
(0 of 22 states)
As expected, this run has no assertion failures ("errors: 0").
Quick Quiz 1: Why is there an unreached statement in locker? After all, isn't this a full state-space search??? Quick Quiz 2: What are some Promela code-style issues with this example? In particular, why does this example have more states than the n=3 case for atomic increment (564 vs. 372)?
Promela Example: QRCUThis final example demonstrates a real-world use of Promela on Oleg Nesterov's QRCU, but modified to speed up the synchronize_qrcu() fastpath. But first, what is QRCU? QRCU is a variant of SRCU (which in turn is a variant of RCU) that trades somewhat higher read overhead (atomic increment and decrement on a global variable) for extremely low grace-period latencies. If there are no readers, the grace period will be detected in less than a microsecond, compared to the multi-millisecond grace-period latencies of most other RCU implementations.
Returning to the Promela code for QRCU, the global variables are as follows: 1 #include "lock.h" 2 3 #define N_QRCU_READERS 2 4 #define N_QRCU_UPDATERS 2 5 6 bit idx = 0; 7 byte ctr[2]; 8 byte readerprogress[N_QRCU_READERS]; 9 bit mutex = 0;This example uses locking, hence including "lock.h". Both the number of readers and writers can be varied using the two "#define" statements, giving us not one but two ways to create combinatorial explosion. The "idx" variable controls which of the two elements of the "ctr" array will be used by readers, and the "readerprogress" variable allows the assertion to determine when all the readers are finished (since a QRCU update cannot be permitted to complete until all pre-existing readers have completed their QRCU read-side critical sections). The readerprogress array elements have values as follows, indicating the state of the corresponding reader:
QRCU readers are modeled by the qrcu_reader() process shown below.
1 proctype qrcu_reader(byte me)
2 {
3 int myidx;
4
5 do
6 :: 1 ->
7 myidx = idx;
8 atomic {
9 if
10 :: ctr[myidx] > 0 ->
11 ctr[myidx]++;
12 break
13 :: else -> skip
14 fi
15 }
16 od;
17 readerprogress[me] = 1;
18 readerprogress[me] = 2;
19 atomic { ctr[myidx]-- }
20 }
A do-od loop spans lines 5-16, with a single guard of "1"
on line 6 that makes it an infinite loop.
Line 7 captures the current value of the global index, and lines 8-15
atomically increment it (and break from the infinite loop)
if its value was non-zero (atomic_inc_not_zero()).
Line 17 marks entry into the RCU read-side critical section, and
line 18 marks exit from this critical section, both lines for the benefit of
the assert() statement that we shall encounter later.
Line 19 atomically decrements the same counter that we incremented,
thereby exiting the RCU read-side critical section.
The following C-preprocessor macro sums the pair of counters forcing weak memory ordering.
1 #define sum_unordered \
2 atomic { \
3 do \
4 :: 1 -> \
5 sum = ctr[0]; \
6 i = 1; \
7 break \
8 :: 1 -> \
9 sum = ctr[1]; \
10 i = 0; \
11 break \
12 od; \
13 } \
14 sum = sum + ctr[i]
Lines 2-13 fetch one of the counters, and line 14 fetches the other
of the pair and sums them.
The atomic block consists of a single do-od statement.
This do-od statement (spanning lines 3-12) is unusual in that
it contains two unconditional
branches with guards on lines 4 and 8, which causes Promela to
non-deterministically choose one of the two (but again, the full
state-space search causes Promela to eventually make all possible
choices in each applicable situation).
The first branch fetches the zero-th counter and sets "i" to 1 (so
that line 14 will fetch the first counter), while the second
branch does the opposite, fetching the first counter and setting "i"
to 0 (so that line 14 will fetch the second counter).
Quick Quiz 3: Is there a more straightforward way to code the do-od statement? With the sum_unordered macro in place, we can now proceed to the update-side process below.
1 proctype qrcu_updater(byte me)
2 {
3 int i;
4 byte readerstart[N_QRCU_READERS];
5 int sum;
6
7 do
8 :: 1 ->
9
10 /* Snapshot reader state. */
11
12 atomic {
13 i = 0;
14 do
15 :: i < N_QRCU_READERS ->
16 readerstart[i] = readerprogress[i];
17 i++
18 :: i >= N_QRCU_READERS ->
19 break
20 od
21 }
22
23 sum_unordered;
24 if
25 :: sum <= 1 -> sum_unordered
26 :: else -> skip
27 fi;
28 if
29 :: sum > 1 ->
30 spin_lock(mutex);
31 atomic { ctr[!idx]++ }
32 idx = !idx;
33 atomic { ctr[!idx]-- }
34 do
35 :: ctr[!idx] > 0 -> skip
36 :: ctr[!idx] == 0 -> break
37 od;
38 spin_unlock(mutex);
39 :: else -> skip
40 fi;
41
42 /* Verify reader progress. */
43
44 atomic {
45 i = 0;
46 sum = 0;
47 do
48 :: i < N_QRCU_READERS ->
49 sum = sum + (readerstart[i] == 1 &&
50 readerprogress[i] == 1);
51 i++
52 :: i >= N_QRCU_READERS ->
53 assert(sum == 0);
54 break
55 od
56 }
57 od
58 }
The update-side process repeats indefinitely, with the corresponding
do-od loop ranging over lines 7-57.
Each pass through the loop first snapshots the global readerprogress
array into the local readerstart array on lines 12-21.
This snapshot will be used for the assertion on line 53.
Line 23 invokes sum_unordered, and then lines 24-27
re-invoke sum_unordered if the fastpath is potentially
usable.
Lines 28-40 execute the slowpath code if need be, with lines 30 and 38 acquiring and releasing the update-side lock, lines 31-33 flipping the index, and lines 34-37 waiting for all pre-existing readers to complete. Lines 44-56 then compare the current values in the readerprogress array to those collected in the readerstart array, forcing an assertion failure should any readers that started before this update still be in progress. Quick Quiz 4: Why are there atomic blocks at lines 12-21 and lines 44-56, when the operations within those atomic blocks have no atomic implementation on any current production microprocessor? Quick Quiz 5: Is the re-summing of the counters on lines 24-27 really necessary??? All that remains is the initialization block shown below:
1 init {
2 int i;
3
4 atomic {
5 ctr[idx] = 1;
6 ctr[!idx] = 0;
7 i = 0;
8 do
9 :: i < N_QRCU_READERS ->
10 readerprogress[i] = 0;
11 run qrcu_reader(i);
12 i++
13 :: i >= N_QRCU_READERS -> break
14 od;
15 i = 0;
16 do
17 :: i < N_QRCU_UPDATERS ->
18 run qrcu_updater(i);
19 i++
20 :: i >= N_QRCU_UPDATERS -> break
21 od
22 }
23 }
This block simply initializes the counter pair on lines 5-6,
spawns the reader processes on lines 7-14, and spawns the updater
processes on lines 15-21.
This is all done within an atomic block to reduce state space.
Running the QRCU ExampleTo run the QRCU example, combine the code fragments in the previous section into a single file named "qrcu.spin", and place the definitions for spin_lock() and spin_unlock() into a file named "lock.h". Then use the following commands to build and run the QRCU model:
spin -a qrcu.spin
cc -DSAFETY -o pan pan.c
./pan
The resulting output shows that this model passes all of the cases
shown in this table:
Now, it would be nice to run the case with three readers and three updaters, however, simple extrapolation indicates that this will require on the order of a terabyte of memory best case. So, what to do? Here are some possible approaches:
The following sections discuss each of these approaches.
How Many Readers and Updaters Are Really Needed?One approach is to look carefully at the Promela code for qrcu_updater() and notice that the only global state change is happening under the lock. Therefore, only one updater at a time can possibly be modifying state visible to either readers or other updaters. This means that any sequences of state changes can be carried out serially by a single updater due to the fact that Promela does a full state-space search. Therefore, at most two updaters are required: one to change state and a second to become confused. The situation with the readers is less clear-cut, as each reader does only a single read-side critical section then terminates. It is possible to argue that the useful number of readers is limited, due to the fact that the fastpath must see at most a zero and a one in the counters. This is a fruitful avenue of investigation, in fact, it leads to the full proof of correctness described in the next section.
Proof of CorrectnessThe proof is as follows:
More Capable ToolsAlthough Promela and Spin are quite useful, much more capable tools are available, particularly for validating hardware. This means that if it is possible to translate your algorithm to the hardware-design VHDL language, as it often will be for low-level parallel algorithms, then it is possible to apply these tools to your code (for example, this was done for the first realtime RCU algorithm). However, such tools can be quite expensive. Although the advent of commodity multiprocessing might eventually result in powerful free-software model-checkers featuring fancy state-space-reduction capabilities, this does not help much in the here and now. As an aside, there are Spin features that support approximate searches that require fixed amounts of memory, however, I have never been able to bring myself to trust approximations when validating parallel algorithms. Another approach might be to divide and conquer.
Divide and ConquerIt is often possible to break down a larger parallel algorithm into smaller pieces, which can then be proven separately. For example, a 10-billion-state model might be broken into a pair of 100,000-state models. Taking this approach not only makes it easier for tools such as Promela to validate your algorithms, it can also make your algorithms easier to understand.
SummaryPromela is a very powerful tool for validating small parallel algorithms. It is a useful tool in the parallel kernel hacker's toolbox, but it should not be the only tool. The QRCU experience is a case in point: given the Promela validation, the proof of correctness, and several rcutorture runs, I now feel reasonably confident in the QRCU algorithm and its implementation. But I would certainly not feel so confident given only one of the three!
AcknowledgementsMany thanks to Suparna Bhattacharya and to Josh Triplett for their careful review of this article. The answers to the Quick Quiz questions are available here. (Log in to post comments)
Using Promela and Spin to verify parallel algorithms Posted Aug 3, 2007 14:05 UTC (Fri) by starblue (guest, #5842) [Link] > If you aren't sure whether your machine has enough memory, run "top" in one window and "./pan" in another.> Keep the focus on the "./pan" window so that you can quickly kill execution if need be. > As soon as CPU time drops much below 100%, kill "./pan".
You may want to use the ulimit command to limit memory use to something safe.
Using Promela and Spin to verify parallel algorithms Posted Sep 8, 2007 23:27 UTC (Sat) by PaulMcKenney (subscriber, #9624) [Link] Excellent point!!! I always like to see how close to the edge I can push the system, but your suggested use of ulimit is well taken.
|
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||