--- layout: fc_discuss_archives title: Message 1 from Frama-C-discuss on July 2013 ---
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>