This project is read-only.

Interpret code with interrupts

Apr 8, 2010 at 7:48 PM

Hi all,

I have trying to apply your lock example in my code to verify a simple interrupt queue (The use of the lock example was inspired by this discussion

The interrupt queue receives events from outside the interrupt manager(hardware or software interrupts).These events are added to the queue (between disable/enable interrupts) or removed and sent to their handlers.

(1) In this example vcc complains about objects that  are not writable before wrapping in the initial function. If all objects are mutable in the initial state, this is suppose to happen?

(2) the queue change only between disable/enable of interrupts and may have a number of instructions or even calls to other functions before enabling interrupts again. If the queue is in a concurrent setting (e.g. many interrupts being inserted), should I use atomic blocks in this instructions? In this case what is the best way to ask vcc to test that those instruction are made atomically ?


typedef struct  entry {
	unsigned int event;
	void *data;

struct queue_entry {
	struct entry sy_event; 

	struct {
		unsigned int pend;
	} asy_events[20];

struct vcc(claimable) vcc(volatile_owns) _CONTAINER { 
  bool interrupt_enable;

  obj_t protected_obj;

  invariant(protected_obj == &queue)
  invariant( interrupt_enable == true ==> keeps(protected_obj) )
} Container; 

//insert and pop functions ...

int init(void)

			 Container.protected_obj = &queue;
	//test queue ...

	return 1; 



Apr 14, 2010 at 10:23 AM
Edited Apr 20, 2010 at 10:07 AM


do you only consider code between disabled and enabled interrupts? then you would not need to model the hardware/interrupt flag at all but just assume that your actions are atomic, i.e. you are already in the sequential domain and can live without claims, atomic blocks etc.

in the other case you should define a volatile abstraction of your system, link this with the implementation using coupling invariants and define all atomic transitions on the state (in your case the queue) via two-state-invariants. disabling interrupts then should give you ownership of the queue, so that you can modify it sequentially and update the volatile spec using an atomic block. I guess your current "Container"-approach would need to be extended then. Maybe others can comment on the technical details if necessary.

Concerning your example i would say you need ownership invariants in the queue object stating that it keeps(&sy_event) and possibly also all the asy_events elements. I'm also not sure if you can directly wrap an array of objects. never tried that out...


hope this helps



Apr 22, 2010 at 2:54 PM

Hi Christoph!

Thanks for your answer. i'm not only consider code between disabled and enabled interrupts, but you're right, if the queue only change without interference(sequential fashion) maybe i will not need  to model the disabled and enabled of interrupts and atomic actions, anyway thanks for the suggestion.

With respect to wrapping(and set the owner) an array of objects i would be grateful if someone could tell me what is the best way to do it.


Apr 22, 2010 at 4:21 PM

Unfortunately, an array of objects a+0, a+1, a+2, ... cannot be wrapped in a single wrap() call since wrap in the current syntax takes only a single object. (I don't know whether the upcoming syntax will support pointer sets). So, an array of objects currently has to be wrapped in a ghost loop (or an assumptions must be stated to that effect). Here's an example:


struct vcc(dynamic_owns) S {
	struct { int a; } t[20];
	invariant(forall(unsigned i; i < 20; keeps(t+i)))

void foo(struct S *s)
		unsigned j;
		for (j = 0; j < 20; j++)
			invariant(j <= 20)
			invariant(forall(unsigned i; i < 20; i < j ? wrapped(s->t+i) : mutable(s->t+i)))

Note that ghost loops (and ghost code in general) must be terminating for soundness reasons. VCC doesn't yet formally check that (and also doesn't currently warn).

Hope this helps, Mark