--- layout: fc_discuss_archives title: Message 1 from Frama-C-discuss on July 2013 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Using frama-c to verify coding patterns of concurrent sw



Sirs


?        I have sw processes (task, thread etc..) as C functions

?        They are called by a scheduler, and will be rescheduled to the first line after the descheduling point [1]

?        So, scheduling is "cooperative", not preemptive (i.e. the "channel drives the scheduling")

?        Local context in each process is allocated on the heap, so state that survive scheduling is stored there

?        I have described a couple of patterns that are interesting to verify with frama-C ...[2], [3]

?        Is it possible to set up an ACSL specification that would be able to verify that certain combinations of local state variables _now_ and certain other combinations _later_ on will sooner or later arrive?

?        Even more than that: I will need to verify more than two steps!

[1] - "New ALT for Application Timers and Synchronisation Point Scheduling" at http://www.teigfam.net/oyvind/pub/pub_details.html#NewALT
[2] -" XCHANs: Notes on a New Channel Type at http://www.teigfam.net/oyvind/pub/pub_details.html#XCHAN
[3] - "The "knock-come" deadlock free pattern" at http://oyvteig.blogspot.fr/2009/03/009-knock-come-deadlock-free-pattern.html

Med vennlig hilsen / Best regards

?yvind Teig
Senior utviklingsingeni?r, siv.ing.  / Senior development engineer, M.Sc.
__________________________________________
Autronica Fire and Security AS
UTC CCS EMEA Fire & Security Operations
Phone: + 47 73 58 24 68 / Mobile +47 959 61 506
E-mail:  oyvind.teig at autronicafire.no<mailto:oyvind.teig at autronicafire.no>
www.autronicafire.no<http://www.autronicafire.no>
www.teigfam.net/oyvind/home/<http://www.teigfam.net/oyvind/home/> (also work-related)

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20130701/850ce37c/attachment.html>