Model Checking a Linked List

Question

I looked in SPIN model checker. However, it does not have features for dynamic allocation. Is there any other model checker that i can use for dynamic allocation?

Answer 1

You can achieve dynamic allocation in a number of ways. In all of them you need to have an upper limit on the number of allocations (that is usually not a limiting factor).

You will define a structure type for the stuff that you want to allocate and you will put a number of these into an array. You will use an index into that array to reference the structure. So, a bit like this:

#define data_t byte

typedef data_record {
  data_t me;
  bool allocated;
  // .... your data fields here ....
}

#define NUMBER_OF_DATA_RECORDS 10

data_record data_record_array[NUMBER_OF_DATA_RECORDS];

#define DATA_RECORD_ALLOCATED(dt)    data_record_array[(dt)].allocated
#define DATA_RECORD_ME(dt)           data_record_array[(dt)].me

Now you can define some inlines to allocate and free these. There are a number of options. For example, to allocate, just iterate through data_record_array to find a data_record that is not allocated. A bit like this:

// Assigns data_ptr with a free data_record index
inline data_record_allocate (data_t data_ptr)
{
   data_ptr = 0; 
   do
   :: data_itr >= NUMBER_OF_DATA_RECORDS -> break
   :: else ->
        if
        :: ! DATA_RECORD_ALLOCATED (data_itr) -> 
           DATA_RECORD_ALLOCATED (data_itr) = true
           DATA_RECORD_ME (data_itr) = data_it
           break
        :: else -> data_itr++
        fi
   od
 }

and then free is like:

inline data_record_free (data_t data_ptr)
{
  DATA_RECORD_ALLOCATED (data_itr) = false
  data_itr = NUMBER_OF_DATA_RECORDS
}

A little more sophisticated would be to put all the free indices, which at the beginning is all indices, into a channel of 'free indices`. When you allocate just read from the channel; when you free just push back onto the channel.