This project is read-only.

Uniprocessor code with interrupt handlers: sequential or concurrent in VCC?

Jul 14, 2009 at 3:12 PM

Hi all,

I've yet some other basic questions (somewhat related to those I posted on last Thu, but it seems cleaner to open a new thread).

(1) When I have code being a system code for a uniprocessor system with interrupt handlers (some code sections have interrupts enabled, others have interrupts disabled): would that be considered a "sequential" or a "concurrent" setting in VCC?

(2) For code that is "sequential" only, does it make sense/is it useful to use claims, or is that restricted to a "concurrent" setting? (Relevance of the answer to this questions depends on the answer to question (1) of course, to get independent of question (1) one also could ask "Does there exist non-trivial (e.g. sequential) code where use of claims is definitely useless/a distraction" ...)

(3) In "VCC: A Practical System for Verifying Concurrent C" it is said (footnote 8): "Claims can actually be implemented using admissible two-state invariants. We decided to build them into the annotation language for convenience". If this is of educational merit, can someone explain on the implementation (if it is trivial) or (alternatively) point to the source (Prelude.bpl/*.cs?) file where they are implemented?


Jul 17, 2009 at 10:11 AM

Hi Holger!

(1) Without knowing the specifics it is difficult to answer your question correctly, but maybe the following thoughts help you decide on your own: the question whether or not something is sequential or not should be asked on the level of data structures. If your interrupt handlers modify some (global) data structures that your code also touches, you are probably in a concurrent context, since in this case you have to deal with the fact, that another "thread" could modify your data without you noticing. So your analysis should probably try to figure out which structures are modified in the code where the interrupts are disabled and if those structures are also touched by the interrupt handlers. So your task is figuring out what is actually protected by the disabling of interrupts.
The disabling of interupts then should transfer the concurrent protected object into a sequential setting, which can only be modified as long as the interrupts are disabled. After enabling the interrupts again the protected object is again in a concurrent setting. Overall this really sounds like another application of a lock pattern which differs in such a way that the "main thread" can always acquire the lock (disabling interrupts) and release the lock by enabling the interrupts. The execution of interrupts implicitly acquires the lock before executing the interrupt handlers code and release it afterwards. But this is done implicitly by the underlying "OS". So verifying that overall protocol could be difficult, but just using that abstraction should be rather straight forward for your code.

(2) Claims do not only serve as a means of ensuring closedness of objects in a concurrent setting, but also have this nice feature that you can pass around additional information about the claimed objects, e.g combining invariants of multiple claimed objects. In a pure sequential context you can model all of that using pre- and post-conditions of functions and tracking the state of the objects in your code, but sometimes claims provide a convenient way of passing information around.
To answer your question: you can use claims in any context but of cause this introduces this overhead of dealing with the claims. So it's up to you to decide to use them in a sequential context if they help you verifying things - use them. In a concurrent context there is basically no way around claims...


Jul 20, 2009 at 8:11 AM
As for (3) in Vcc/Test/testsuite/examples/Handles.c you can find an implementation of a handle, which is a claim, preventing something from being open, but without an additional property. Should you want additional properties, you would need multiple handle types, which is why we built them in. The actual implementation of claims in VCC sits in multiple places in the compiler and prelude, so unfortunately it's difficult to point you to a single file.
Jul 20, 2009 at 9:30 AM

Handles.c is currently (2009/07/20) not part of the installer and can only be accessed by downloading the sources. I just modified the installer to also copy this file to the "VCC Samples" directory in the users home directory. This change will be part of tomorows drop.

Jul 24, 2009 at 12:49 PM
Edited Jul 24, 2009 at 1:12 PM


just to give some follow-up, by the criterion you gave whether interrupt handlers do (not) modify some global data structures that are also modified by the code when interrupts are enabled (+ that there are no race conditions of read-write type between interrupts and non-interrupt code), the code currently under examination could indeed by classified as "sequential". As you wrote, that does not rule out that "concurrent" methodologies may be more "natural".

Thanks, Holger

Jul 24, 2009 at 1:24 PM

Hi Holger,

I'm just wondering: what is the point of disabling the interrupts then? I assume there is a very good reason for disabling the interrupts for a brief period of time in your code.
In most cases I acutally encountered disabling of interrupts, this was usually to prevent race conditions between an interrupt routine and some other code. Therefore disabling interrupts indicates in my opinion that you are much more likely to be operating in a concurrent setting than in a sequential setting... But this of cause really depends on what your code is actually supposed to do.


Jul 24, 2009 at 2:17 PM

Hi Markus,

I wrote (actually distorting your original suggestion) that it was checked whether it holds when interrupts are *enabled*. I see now it is needed to check this for both enabled (just a basic sanity condition) and disabled (the potentially more interesting condition). Can confirm now (thanks also to alex!) that indeed it does *not* hold for code where interrupts are disabled. And I thus correct quickly myself from "sequential" to "concurrent", so your intuition was correct from the beginning. Thanks for your guidance.