List Remove

May 23, 2012 at 12:33 PM

I read the VCC tutorial and tried to enhance the list implementation of the tutorial with a remove method. However, I encountered some problems with verifying this method.

Note: I used the same loop invariant as used in the 'member' function in the tutorial, and the same 'list' struct with identical VCC annotations. I did not yet specify any changes in the followers map, since the problem I have is encountered before the map should be changed.

The code:

int list_remove(struct linked_list* list, int item)
    _(requires \wrapped(list))
    _(ensures \wrapped(list))
    _(ensures \result != 0 ==> list->val == \old(list->val))
    _(ensures \result == 0 ==> !list->val[item])
{
        struct node* head = list->head;
        struct node* n = head;
        while (n != NULL)
            _(invariant n != NULL ==> n \in list->\owns)
        {
            if (n->next == NULL) {
                return -1;
            } else {
                int next_val = n->next->value;
                if (next_val == item) {
                    struct node* tmp = n->next; //tmp is the node to be removed
                    n->next = n->next->next;
                    _(ghost {
                        list->\owns -= n->next;
                        list->val[item] = \false;
                    })
                    free(tmp);
                    return 0;
                } else {
                    n = n->next;
                }
            }
        }
        return -1;
    }

The problem I have is with the following line:

  n->next = n->next->next;

VCC returns the following error:

'Assertion 'n->next' is writable did not verify.'

The documentation of the 'member' function in the tutorial (p.77) states:

"...,the invariant of the list tells us that by following the next pointer
we stay in the owns set".

I also believe that, in the 'member' function, all that's needed to prove n is writable to verify the call 'n = n->next' is to prove that n in list->\owns. So, I thought, the list invariant proves n->next in list->\owns and thus n->next is writable, but this seems not to be the case.

Does anybody have an idea on how to make n->next writable in this situation?

Editor
May 23, 2012 at 4:19 PM
Edited May 23, 2012 at 4:49 PM

Hi,

I don't know how helpful my reply is going to be as I have no solution to suggest, but I can point out two things that jumped out when reading your annotations.

The first one is that the invariant you placed on the loop is very weak, and indeed looks too weak to preserve thread locality (necessary for reading data). In addition, since the list is not local to the function, I believe you are required to specify that the loop's body may write its contents using a _(writes ...) contract.

The second issue I see is that you keep the list wrapped throughout your function, and can therefore not expect it to be writable. A possible solution would be to use each iteration of the loop, as it walks through the list looking for the element to remove, to unwrap each node in turn, until the desired node is found (and you probably want to unwrap that one as well so you can free it). You should then be able to update the next pointer of the current node (the removed node's parent) and leave the loop. And now you are faced with the problem of walking backwards through your list to re-wrap all of its nodes so you can guarantee the post-condition. One possibility for this would be to keep a ghost list of the nodes you unwrapped, in reverse order, and you can just, in ghost code, walk through that list and re-wrap each node in turn. I expect your invariants to blow up for that.

Disregard the above: I replied without looking at the spec for the list tutorial, and it doesn't apply: you only need to unwrap the list object itself, and the one element you want to modify, since the ownership structure is in fact flat.

I'll try to come back with a more constructive reply in a bit, but feel free to try to act on my suggestions if they aren't too obscure.

In any case, welcome to VCC!

Francois

Second Edit: As a side-note, your specification does not say that, "if item is in the list, then it will be removed" (it just says "if the function returns 0, then item is not in the final list"). In fact, your function would not remove item if it's at the head of the list. It's still a good exercise, though.

Editor
May 25, 2012 at 10:45 AM

Hi again,

I've given this a longer thought and look and there are many more problems you need to deal with, either by restricting the cases in which the function can be called using a precondition or additional invariants on the list structure, or by being extra careful when you write the code (adding dynamic checks, for example). Here is a short list of the main issues I found (there may be more).

  • Nothing in the invariant of the strucure or in the precondition prevents the list from having several copies of the same integer. Do you intend to remove all of them, or just the first copy? In the former case, you need to modify your code to keep looping after the first one has been found, and until the list is indeed empty. In the latter case, you need to change your postcondition.
  • Nothing in the invariant of the structure or in the precondition prevents the list from having a cycle. This causes issues with ownership and the followers field if the object you remove is actually sitting at the head of the cycle. In fact, it may even cause issues in the interpretation of removing a node (for example, if the removed node has an edge to itself, setting its parent's next field to its next field is not going to be changing anything). This is more of a philosophical question, and I would strongly encourage you, in a first sitting, to just forbid cycles using an invariant on the list. Making sure that the other functions work with the acyclicity invariant sounds like a much more gentle exercise than implementing a remove operation on a general unconstrained data structure.

I can help if you have specific questions, but I also encourage you to keep posting them on here: I am far from being the foremost expert on VCC.

Cheers,
Francois

May 25, 2012 at 7:27 PM

Hi Zetsubo, Francois,

for giving some ideas on how to experiment with ghost code for singly-linked lists it also might be helpful to point out that a more fully specified doubly-linked-list (List.c/List.h) including removal of elements exists in the VCC repository Test suite. We had happily used a predecessor (old VCC syntax) for verification of some OS-based code here. I would join Francois in being interested in any follow-up. Best, Holger

May 27, 2012 at 7:38 PM

Thanks a lot for the replies guys!

Unfortunately, I have been busy with some other work, so I didn't have time to look at this again or reply sooner. In fact, I won't be able to pick up VCC again till later this week. But I will keep you updated if I make some progress over the week.

I know the invariants and contract are far from sufficient at the moment, but I thought it best to first fix my ownership error before starting to work on the more interesting (and undoubtedly more difficult) stuff.

Update coming soon!

Developer
May 28, 2012 at 4:36 PM

My bad, I had intended to put into the tutorial a note that the invariants of the list there aren't good enough for node removal, but that edit somehow got lost. The invariants for lists in the tutorial are indeed rather unusual; if I recall, they were done this way so that the abstract value of the list qua set could be obtained directly from the follower relation, without having to project it to the value stored in the nodes (which would incur either an existential quantification or maintaining an additional ghost variable). This was probably a bad idea.

The normal way to implement a list is to maintain the (non-transitive) reachability relations for nodes (rather than for values stored in the nodes), and to have an invariant that nodes don't reach themselves. This allows you to delete as well as add.

Developer
Jul 3, 2012 at 11:58 PM

The latest version of the tutorial (available with the source distribution) has a list invariant that is sufficient for node removal.

Jul 9, 2012 at 2:32 PM
Edited Jul 9, 2012 at 2:34 PM

Sorry for the late reply, but the past month was pretty busy with exams so I didn't have the time yet to look at this again. But I did manage to get a look at it the past few days and here's a small summary of what I changed.

I used the invariants for the List as they appear in the new tutorial. To facilitate removal, I wanted each value to be unique in the list. For that purpose, I added the follwing invariant to the list:

 // Each element in the list is only contained once.
 _(invariant \forall Node *n, *m; {\mine(n), \mine(m)}
        \mine(n) && \mine(m) && n != m ==> idx[n] != idx[m] && n->value != m->value)

I constructed this invariant analogous to the invariant in the double linked list example provided by holgerblasum. This invariant did not break the add and member functions from the tutorial so I assume it is correct, but if anyone spots any errors in it please let me know.

I then wrote the following contract for the list removal function:

int list_remove(List* list, int item)
 _(requires \wrapped(list))
 _(ensures \wrapped(list))
 _(ensures \result != 0 ==> list->val == \old(list->val))
 _(ensures \result == 0 ==> (\forall int p; list->val[p] <==> (\old(list->val)[p] && p != item)))
//If removal succeeds, all previous values remain except 'item')
 _(writes list)

Because values should now be unique, removing the desired item from the val mapping should be enough to guarantee removal.

Below is part of the body of the removal function:

(Note: this part is executed when the node to be removed is not the head of the list)

Node* current = head;
_(assert \inv(list))
while (current != NULL)
    _(invariant current ==> current \in list->\owns && current \in \domain(list))
    _(invariant  \forall Node *m; m \in list->\owns && m->value == item
        ==> m == current->next || (current && list->idx[m] > list->idx[current]))
    //invariant now states that node with value 'item' can only be next node further down the list
               
{
    if (current->next == NULL) return -1; //ERROR - should not occur
    _(assert current->next \in list->\owns)
    _(assert current->next \in \domain(list))
    int next_val = current->next->value;
    if (next_val == item) { //current->next is the node to be removed
        Node* tmp = current->next;
        _(assert current->next \in list->\owns)
        _(assert current->next \in \domain(list))
        _(unwrapping list) {
            current->next = current->next->next;
        }
        _(ghost {
            list->\owns -= tmp; //Remove node of item from ownership
            list->val[item] = \false;
        //Depths of nodes after removed node are decreased, others remain the same.
            list->idx = (\lambda Node *m; list->idx[m] > list->idx[tmp] ? list->idx[m] - 1 : list->idx[m]);
        })
        return 0;
    } else {
        current = current->next;
    }
}

I used the same invariants in the while loop as those used in the traversal loop of the member function, with one smal adjustment in the second invariant: I changed m == current to m == current->next. My reasoning was that the original invariant states that if a node exists with 'item' as value, then that node is either equal to the current node in the loop or further down the list. But in this case, since I check whether the next node is the node to be removed, this invariant should be changed to: the node containing 'item' is either the next node of current, or further down the list.

My entire file can be viewed at https://www.dropbox.com/s/97ubhnbw68b34mp/vcc_iterative_final.c

Currently, I am left with one error during verification. In the assignment current->next = current->next->next, current->next is still not writable. The tutorial says that, during unwrap: 'for each object o owned by p, set o->\owner to \me and add o to the
writes set' is done. So I reasoned that when current->next is in the \owns set of list and I unwrap list, current->next should become writable. But this does not seem to be the case.
Can anyone see what I am doing wrong here?

Thanks in advance!

Developer
Jul 13, 2012 at 1:16 AM

Hi Zetsubo,

Unwrapping the list made current writable, but not current->next, because current is still wrapped. You have to unwrap current also before writing to current->next.

(Now that you mention it, I will also fix the tutorial to say that unwrapping an object also makes its fields writable.)

hope this helps, ernie

Jul 15, 2012 at 10:08 AM

Doh, silly me, of course that was the problem. Can't believe I didn't spot that :)

List removal now verifies. Thanks a lot!

 With that function taken care of, I tried my luck with some other functions, but I ran into some trouble there.

 1) I'd like a get_item function. The index of a certain item can be extracted from the idx mapping, but this mapping was declared as type \natural, and I want to compare its results to an int. For example, when using get_item to get the item at index i, I'd use the following ensures clause:

 _(ensures \result == \exists Node* m; list->idx[m] == i ==> m->value)

in other words, the result of the get_item function is the value of the node whose index equals int i. But this obviously doesn't work, because I'm comparing an int with a \natural.

 Is there any way to convert one to the other, or shoud I redeclare the idx mapping as type int?

 

- I also added an append function, which adds a new item to the end of the list. After adding, I adjust the idx mapping in ghost code to reflect the adding. I wrote:

 list->idx = (\lambda Node *m; m == newNode ? (list->idx[current] + 1) : list->idx[m]);

 Current is the node after which the new item is appended (using the assignment current->next = newNode). So if Node m equals the new node, idx[m] == idx[current] + 1, else the indices remain the same.

However, verification shows that the invariant concerning the idx mapping in the List structure does not hold when the list object is re-wrapped. Is there something wrong with my adjustment of the idx mapping here?

 Full code can be found here:

 https://www.dropbox.com/s/54bzjw7gedis9pz/vcc_iterative.c

 

Thanks in advance!