Hanbing Liu, May 5, 2004 [updated Mon May 3 17:39:39 2004] SHORT ABSTRACT ============== This coming Wednesday, I will present my formalization of a ring data structure in ACL2. I will describe a mechanically checked proof about it briefly. We proved that "join" (add a new node to a ring) and "rm" (remove a node from a ring) primitives maintain the unidirectional ring topology. Because the ring concept is formulated in terms of reachable sets from different nodes, the proof revolves around reachability on a graph in a certain representation and how the reachability changes when the graph is updated. This work is motivated by Xiaozhou (Steve) Li's ACL2 Seminar presentation of "Concurrent Maintenance of Rings" on March 03, 2004. It can be considered as a small initial step towards a mechanically verified ring maintenance protocol in ACL2. SUMMARY ======= The system of interest is comprised of a set of nodes. Each has a neighbor pointer. Certain system configurations can be recognized as representing a unidirectional ring. We need to show primitives that adds new node and removes some node preserve the unidirectional ring-ness. Representation -------------- The set of nodes and their neighborhood information can be modeled and recorded in a list of pairs. The first component pair records the name of a node, the second component records the reference to the neighbor of the node. For example: L = (( A . B ) ( B . C ) ( C . A ) ( D . nil) ( E . X)) represents a system configuration with 5 nodes. From A's neighbor is B, B's neighbor is C and so on. D, E do not have any neighbor. Ring Definition --------------- In my formulation, a system configuration represents a ring, if and only if, starting from any node that has a neighbor, all nodes with a neighbor are reachable. ------------------------------------------------------------------- (defun ring (l) (non-nil-neighbor-set1 (all-nodes l) l)) (defun ringp-aux (l1 l ring) "Test whether any nodes in l1's reachable set is set-equal to ring" (declare (xargs :measure (len l1))) (if (endp l1) t (and (set-equal (reachable-set1 (car l1) l nil) ring) (ringp-aux (cdr l1) l ring)))) (defun ringp (l) "Assert all nodes on the ring can reach all other such nodes" (ringp-aux (ring l) l (ring l))) ------------------------------------------------------------------- Thus, the system configuration L is a ring. A, B, C form a "ring". D, E are not on the ring. Update Primitives ----------------- Join(n, s, e, l) is a primitive that updates a system configuration. (defun join (n s e l) "set node n's neighbor to s, set node e's neighbor to n" (bind e n (bind n s l))) Join adjusts n's neighbor to s, and adjust e's neighbor to n in a system configuration l. Join(E, A, C, L) transforms L in to new system configuration: (( A . B ) (( A . B ) ( B . C ) ( B . C ) ( C . A ) ====> ( C . E ) ( D . nil) ( D . nil ) ( E . X)) ( E . A)) For "join", we show (defthm join-preserve-ringp (implies (and (not (mem n (ring l))) (ringp l) (alistp l) (mem e (ring l)) (mem s (ring l)) (assoc-equal n l) (equal (cdr (assoc-equal e l)) s)) (ringp (join n s e l))) when if e's neighbor is s, if e, s are on ring, node n is not on the ring, the resulting system configuration represents a ring with n as an additional node. Similarly "rm" is defined as (defun rm (s a l) (bind a nil (bind s (cdr (assoc-equal a l)) l))) which adjusts s to point to the neighbor of a, and update a's neighbor to nil Short Proof Sketch ------------------ For JOIN: 1. Prove that updating the neighbor field of a node, which is not on the original ring, does not change the ring. 2. Prove that a reachable-set can be decomposed into two segments. 3. Show the segment before the node, which is being updated, does not change from what it was. Show the new second segment is extended with a new node -- when the new node's neighbor is the original neighbor of the node being updated. 4. Prove that after join, the set of nodes reachable from a node on the ring is equal to the set of nodes on the ring. For RM: 1. Prove that our reachable-set is in fact a path through a graph. The path is a simple path. 2. Prove that there is a unique simple path between two nodes. 3. Prove that the reachable-set is equal a concatenation of two segments. One segment ends with the node to be skipped. 4. Prove that the reachable-set after "rm" operation is a concatenation of two segments 5. Prove that DEL a node from the concatenation of two segments from 3 gives us the concatenation of two segment that happens to equal to those from 4. 6. Prove that one and only one node, which has a neigbor originally, become neighborless after "rm" Comments and Discussion ----------------------- * Other possible representation/definition/proof strategy * Reachability and ACL2 definition principle ;----------------------------------------------------------------------