#verified programming

[vc3d]

Initializing the \owns set

I want to point out one issue I had a long while back because I don't think I've mentioned it yet.

The _(dynamic_owns) examples in the tutorial document do not show how to initialize such an object. Particularly, how to initialize the \owns set. Here is an example:

SafeContainer* a; //...malloc and other such things here...// _(ghost a->\owns = {}; )

The \owns set must be initialized with {} before it can be used and before the object can be wrapped, but it's as simple as that :-)

After some confused searching, I found this in the manual document (found here), section 8.1, in the rough definition of "wrap".

[vc3d]

Array Objects and _(dynamic_owns)

I just finally got some of my Mesh object invariants and code to verify!

A few weeks ago while working on this, I decided to take a step back to look carefully at the SafeString and SafeContainer objects in the VCC tutorial document (found here). This helped, but I wound up confusing myself over the syntax and meaning of so-called "array objects."

In SafeContainer's struct definition:

struct SafeString **strings; unsigned len; _(invariant \mine((struct SafeString*[len])strings))

In code initializing a SafeContainer before wrapping it:

_(ghost a->\owns += (SafeString[a->len])a->strings; )

Note that SafeContainer's "strings" field is meant to point to an array of pointers to SafeStrings, not an array of SafeStrings. My Mesh object contains arrays of other objects, not pointers to other objects. While SafeContainer's array of pointers (pointers are not "first class objects" as described in the tutorial) needs to be wrapped into an array object and the array object added to SafeContainer's \owns set explicitly, my Mesh object's arrays are made of first class objects which can be directly added to Mesh's \owns set. No encompassing array object is needed, though I have tried adding the appropriate invariant and \owns+= operations and it does not seem to hurt.

My largest mistake was assuming that if I wrapped and managed ownership of an array object encompassing an array of first class objects, that VCC would take that as a shortcut for wrapping and adding the individual objects within, but this seems not to be the case. I must explicitly add and wrap all individual objects within my arrays (and in fact, the array objects are not even required). The assumption I made has had me running in circles for weeks.

Copied here is a sort of simplified toy version of my Mesh class which I used to figure out what was wrong, but without so much clutter. The PairLists object contains two lists of Pair objects and the invariant specifies that all Pair objects in the first list should point their "pair" member pointers at other Pair objects which point back to the objects in the first list... they should each have a symmetric pair. The initialization function builds a valid PairLists object, storing the pairs for the first list into the second list. Note that I have no invariant on the second list, so it may contain arbitrary elements. See my comments for additional notes.

#include <vcc.h> #include <stdlib.h> //malloc typedef unsigned int uint; typedef struct Pair Pair; typedef struct Pair { Pair* pair; } Pair; typedef _(dynamic_owns) struct PairLists { uint num1; uint num2; Pair* pairarray1; Pair* pairarray2; //OWNERSHIP //THESE DO NOT HELP HERE //_(invariant \mine( (Pair[num1]) pairarray1) ) //_(invariant \mine( (Pair[num2]) pairarray2) ) //These invariants on ownership, when uncommented, help see whether the ownership or pair condition portion of the following invariant is failing when it fails. //_(invariant \forall uint i; // i < num1 // ==> // \mine(&pairarray1[i]) //) //_(invariant \forall uint i; // i < num2 // ==> // \mine(&pairarray2[i]) //) _(invariant \forall uint i; i < num1 ==> \mine(&pairarray1[i]) && \mine(pairarray1[i].pair) && \mine(pairarray1[i].pair->pair) && pairarray1[i].pair->pair == &pairarray1[i] //pair's pair points back to pair ) } PairLists; void PairListInit(PairLists* dis) _(writes \extent(dis)) _(ensures \wrapped(dis)) { _(ghost dis->\owns = {};) dis->num1 = 2; dis->num2 = 2; dis->pairarray1 = malloc(dis->num1*sizeof(Pair)); dis->pairarray2 = malloc(dis->num2*sizeof(Pair)); //Ignore malloc failure for the sake of testing the rest of this stuff concisely _(assume dis->pairarray1 != NULL) _(assume dis->pairarray2 != NULL) //Initialize the pairs //If any of these following few lines are removed, the PairLists's pairing invariant is not satisfied. Comment any of these to test that the invariant is working correctly. dis->pairarray1[0].pair = &dis->pairarray2[0]; dis->pairarray2[0].pair = &dis->pairarray1[0]; dis->pairarray1[1].pair = &dis->pairarray2[1]; dis->pairarray2[1].pair = &dis->pairarray1[1]; //Set \owns //THESE DO NOT HELP HERE //_(ghost dis->\owns += (Pair[dis->num1])dis->pairarray1;) //_(ghost dis->\owns += (Pair[dis->num2])dis->pairarray2;) _(ghost dis->\owns += &dis->pairarray1[0];) _(ghost dis->\owns += &dis->pairarray1[1];) _(ghost dis->\owns += &dis->pairarray2[0];) _(ghost dis->\owns += &dis->pairarray2[1];) //THESE DO NOT HELP HERE //_(wrap (Pair[dis->num1])dis->pairarray1) //_(wrap (Pair[dis->num2])dis->pairarray2) _(wrap &dis->pairarray1[0];) _(wrap &dis->pairarray1[1];) _(wrap &dis->pairarray2[0];) _(wrap &dis->pairarray2[1];) _(wrap dis) }

[vc3d]

Verifying code with malloc()

I have been trying to sort through the task of verifying C code (using VCC) which allocates heap memory.

First, I tried naively using objects created via malloc(). I found that you must consider the possibility that malloc returns NULL because of some problem allocating enough room for the structure. This yields errors like "error VC8020: 'dis->verts' is not writable before wrapping it." because of the chance that dis->verts was just set to NULL rather than to a valid writable portion of memory. I temporarily worked around this by _(assume pointer != NULL) following calls to malloc(), but this is not a solution. However, it is enough for the code to verify in most circumstances and reflects my usual lack of concern for program stability when memory is exhausted.

I next found that malloc behaves oddly if you pass it a 0 argument. In this case malloc does not necessarily return NULL, but yet the address it returns may still not be mutable nor writable. It is not enough to _(assume ) that the pointer is not NULL.

error VC8020: 'dis->edges' is not writable before wrapping it. error VC9502: Call 'wrap dis->edges' did not verify. error VC9599: (related information) Precondition: 'the object being wrapped is mutable'.

I can _(assume ) both of these, but it is better to add some control logic to ensure I don't try allocating zero memory.

[vc3d]

A few days ago I had most of the basics of the client application complete. There remains some problem with my generation of the perspective transformation matrix (why the view isn't showing that colored triangle correctly), but there is enough of the functionality that verification issues and verification design requirements manifest.

I began adding invariants to the various datastructures. I was hung up on some things (inadmissible invariants that seemed correct in all other ways), but realized the situation demanded that the structures be annotated with _(dynamic_owns).

[vc3d]

HalfEdge

The bare bones of a HalfEdge structure are in place. It took some fiddling with C struct syntax that was not familiar to me (forward declaration, typedef of struct), but now that it works it's clear.

I have to pick a set of mesh edit operations for the program. These would be things such as Collapse Edge or Extrude Face. An artist user would use these abilities to shape a mesh.

I need to specify invariants for the HalfEdge structure, or perhaps for an encompassing Mesh structure. Half Edge can only represent a manifold surface.  That is, the local area around any point should have the topology of a disk.  I should be able to encode this as invariants for a mesh structure.

More sophisticated structures like the "Winged-Edge" structure are needed for more complex non-manifold mesh representations, but I don't plan on implementing that... at least not in the initial version of this application.

[vc3d]

I have been working on understanding the process of verifying concurrent linked structures.

As an exercise, I am verifying the non-blocking queue structure described in "Simple, Fast, and Practical Non-Blocking and Blocking Concurrent Queue Algorithms" by Maged M. Michale and Michale L Scott (Department of Computer Science, University of Rochester).

I was told that verification of the algorithm has been done by others, so I have some faith that I will succeed :P

[vc3d]

Verified C 3D

For part of my undergraduate education, I learned to use Maya 2008 for 3d-modeling.

Remembering to press Ctrl-S every few minutes was one of the more important parts of the artistic process in that piece of software.  I distinctly remember suffering the terror of clicking on an item in Maya to find that the UI becomes unresponsive… or maybe suddenly seeing my wallpaper — the Maya window nowhere to be found.

Remembering those days, I have set out to create a simple, reliable 3d modeling platform programmed in C with Verified Concurrent C (VCC) verification guaranteeing the stability of the software.  I think this project will be a fun way to explore the process of writing verified code.  It will also be a C-programming learning experience for me, as the bulk of my experience is in C++ and C#.

This might not be the most inspiring or typical use of VCC, but I think its intent can resonate with users of creative software.