|
Contraint-based Automatic Symmetry Detection |
Shao Jie Zhang, Jun Sun, Chengnian Sun, Yang Liu, Junwei Ma and Jin
Song Dong
Overview
This page contains supplementary material for our paper: ”Contraint-based Automatic Symmetry Detection for Model Checking”.
This page is maintained by Shao Jie Zhang
.Supplementary Material
The technical report of our paper is here
Experiment Results
We evaluate the effectiveness of our detection approach on a wide list of systems. They are obtained on a laptop running Linux Debian with Intel Core 2 Duo 2.8GHz and 3.8 GB memory. The examples are introduced in the following.
- Reader-Writer problem [1].
The first example focuses on partially symmetric systems. We borrow a variant of Reader-Writers problem from [1]. The problem consists of reader processes (with ids 0 to N-2) and one writer process with id N-1. Every process may attempt to reach the critical section. If no process is currently in th critical section, any process can enter it. A reader process can also enter the critical section as long as the writer process is not in it. Thus these processes are quite similar but slightly different. The global behavior of the system is not totally but approximately symmetric. - Peterson’s mutual exclusion protocol [2].
The N-process protocol manipulates shared arrays in such a way that it eliminates at least one process trying to access the critical section per round in a total of N −1 rounds until
only one remains, so that it guarantees that no more than one processes are in the critical section at the same time. - A prioritized resource allocator [3].
The system consists of N client processes and one resource allocator process. It has a star topology and all the clients only communicate with the resource allocator. Each client has a priority level and may send requests for accessing the resource to the resource
allocator. When the resource allocator receives multiple requests, it always grants access to the request from the client with the highest priority. If all the requesting clients have the same priority level, the allocator chooses one request in a nondeterministic way. A configuration is written in the form a0−a1−···−ak−1, where client processes 0,1,··· ,a0 have priority level 0, a0+ 1,a0+ 2,··· ,a1 have priority level 1, etc. - Message routing in a hypercube network [3].
Hypercube is a popular implementation model of parallel computation applications. A d-dimensional hypercube is a special case of a d-dimensional n1× n2× ··· × nd array when ni = 2 for 1 ≤ i ≤ d. The hypercube has 2d processors, each of which is directly connected to d other neighboring processors. The identifier of a processor node is a binary string (x1,x2,··· ,xn). Two nodes are neighbors if and only if their identifiers differ in only one position. The protocol models a parallel system where messages are routed through the hypercube architecture. Upon receiving a message attached with the id x of the recipient, a node checks its own id with x. If they are the same, the node would process the message. Otherwise, the node would forward the message to its neighbor whose id differs from x only in one bit position. For example, a messages is sent from a node (0,0,0) destined for a node (1,1,1). The track of this message may be (0,0,0) → (0,1,0) → (1,1,0) → (1,1,1). The system is highly symmetric and has 2d× d! automorphisms. A configuration is denoted by the number of dimensions of the hypercube. Note that the configuration d is composed of 2d processes. - Server-client system in a three-tiered architecture [3].
As its name implies, the systems has three layers, one for client processes, ne for server processes and one for the process representing the data storage system. Each process has two channels, one for receiving incoming requests and the other for sending queries to other processes in the neighboring layer. A client repeats the sequence of operations of sending a request message to the server it is connected to and waiting for receiving a response message from the server; a server repeats the sequence of operations of receiving request from a client it is connected to, sending a query to the database, receiving data and sending a response message to the client; the database repeats the sequence of operations of receiving a query from a server and sending back data to the server. for each experiment of the system is written in the form a1−a2−···−ak, which denotes that the system consists of k server processes and ai clients connected to server i. - Dining Philosopher Problem [4].
The N philosophers sit at a circular table with a large bowl of spaghetti in the center. A fork is placed in between each philosopher, and as such, each philosopher has one fork to his left and one fork to his right. As spaghetti is difficult to serve and eat with a single fork, it is assumed that a philosopher must eat with two forks. The philosopher can only use the fork on his or her immediate left or right and he can only put down the forks after eating. - Miler’s scheduler [5].
There are N processes, which are activated in a cyclic manner, i.e., process i activates process i + 1 and after process n process 1 is activated again. Moreover, a process may never be re-activated before it has terminated. The scheduler is built from n cyclers who are positioned in a ring. The first cycler plays a special role as it starts up the system. - Non-deterministic two-hop coloring protocol in rings [6].
It is a protocol to make nodes to recognize their neighbors in a ring. In fact, it is a general algorithm that enables each node in a degree-bounded graph to distinguish between its neighbors. The graph is colored such that any two nodes adjacent to the same node have different colors. More precisely, for each node v, if u and w are distinct neighbors of v, then u and w must have different colors. (u,w) is called a two-hop pair. - Self-stabilizing leader election protocol in complete graph [7].
Each agent has one bit of memory, denoting being the leader or not. There is a leader detector in the network to signal the presence of a leader and to broadcast a boolean value corresponding to the signal to each agent. The detector is not guaranteed to give correct answers all the time, but it will eventually give a correct answer permanently. This protocol guarantees that a unique leader will eventually be elected. - Self-stabilizing leader election protocol in directed rooted trees [8].
This system models a leader-election algorithm for directed rooted tree of odd size. - Self-stabilizing leader election protocol in ring [7].
This system models a leader-election algorithm for network rings using a leader detector. - Hanoi puzzle.
The tower of hanoi is a classic mathematical puzzle. It consists of three pegs and a number of disks N of different sizes can be put onto a peg. You may move the top disk from one peg to the top of another peg at a time. At no time can a larger disk be put on top of a smaller disk. Initially, all disks are stacked at one rod(called the initial rod) in order from the largest at the bottom to the smallest at the top. The other two rods are empty. The goal is to find the minimum number of moves to move all the disks to another rod. - Scheduling the social golfer problem [9].
The social golfer problem was first posted on sci.op-research in May 1998. It is a famous combinational optimization problem. The task is to schedule N = G × P golfers into G groups of P players in W weeks, such that no two golfers play in the same group more than once. Here we consider a heuristic tabu-search scheduling algorithm for this problem proposed in [9]. It consider a special case of the problem where G is a prime, S = G and W = G + 1. For week 0, the schedule is generated randomly such that each position has one distinct golfer. For any following week w, any group i, any position j, the algorithm chooses the golfer in week 0 whose position is (i+(w -1)×j) mod S in group j. A configuration of the system is written in the form G-S-W where G is the number of groups, S is the number of golfers in one group and W is the number of weeks.
