From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.org/gmane.linux.lib.musl.general/6036 Path: news.gmane.org!not-for-mail From: Alexander Monakov Newsgroups: gmane.linux.lib.musl.general Subject: Re: sem_getvalue conformance considerations Date: Mon, 1 Sep 2014 21:50:16 +0400 (MSK) Message-ID: References: <20140827023338.GA21076@brightrain.aerifal.cx> <1409123141.4476.18.camel@eris.loria.fr> <20140827074310.GK12888@brightrain.aerifal.cx> Reply-To: musl@lists.openwall.com NNTP-Posting-Host: plane.gmane.org Mime-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII X-Trace: ger.gmane.org 1409593950 31882 80.91.229.3 (1 Sep 2014 17:52:30 GMT) X-Complaints-To: usenet@ger.gmane.org NNTP-Posting-Date: Mon, 1 Sep 2014 17:52:30 +0000 (UTC) To: musl@lists.openwall.com Original-X-From: musl-return-6043-gllmg-musl=m.gmane.org@lists.openwall.com Mon Sep 01 19:52:19 2014 Return-path: Envelope-to: gllmg-musl@plane.gmane.org Original-Received: from mother.openwall.net ([195.42.179.200]) by plane.gmane.org with smtp (Exim 4.69) (envelope-from ) id 1XOVlu-0008U3-PC for gllmg-musl@plane.gmane.org; Mon, 01 Sep 2014 19:52:06 +0200 Original-Received: (qmail 7445 invoked by uid 550); 1 Sep 2014 17:52:05 -0000 Mailing-List: contact musl-help@lists.openwall.com; run by ezmlm Precedence: bulk List-Post: List-Help: List-Unsubscribe: List-Subscribe: Original-Received: (qmail 7437 invoked from network); 1 Sep 2014 17:52:05 -0000 In-Reply-To: User-Agent: Alpine 2.00 (LNX 1167 2008-08-23) Xref: news.gmane.org gmane.linux.lib.musl.general:6036 Archived-At: Hi, If there's interest, my basic model file for semaphores in Promela/Spin is pasted below. Perhaps if I started doing this earlier it would help to avoid some mistakes. // spin -a sem.pml && gcc -O2 -DSAFETY pan.c && ./a.out typedef sem_t { int value, waiters; // Behavior int val0, val1; // Implementation }; sem_t sem; #define sem_invariants ( \ (sem.value >= 0 && sem.waiters >= 0) && \ (sem.value == 0 || sem.waiters == 0) && \ sem.val0 == sem.value - sem.waiters && \ sem.val1 >= 0) bool done; active proctype monitor() { do :: d_step { !sem_invariants -> assert(0); } :: done -> break; od } inline sem_trywait(retval) { // d_step sequences are not preemptible if :: d_step { sem.val0 > 0 -> sem.val0--; sem.value--; retval = 0; } :: else { retval = -1; } fi } inline sem_post() { int v; d_step { v = sem.val0; sem.val0++; if :: v >= 0 -> sem.value++; :: v < 0 -> sem.waiters--; fi } if :: v < 0 -> sem.val1++; :: else fi } inline sem_wait(interruptible, retval) { int v; d_step { retval = 0; v = sem.val0; sem.val0--; if :: v > 0 -> sem.value--; :: v <= 0 -> sem.waiters++; fi } if :: v <= 0 -> if // non-deterministic if interruptible && sem.val1 > 0 :: d_step {sem.val1 > 0 -> sem.val1--;} :: interruptible -> d_step { v = sem.val0; if :: v < 0 -> sem.val0++; sem.waiters--; retval = -1; :: else fi } if :: v >= 0 -> d_step {sem.val1 > 0; sem.val1--;} :: else fi fi :: else fi } int n_posts, n_waits, n_waitfails; proctype waiter(bool interruptible) { int retval; n_waits++; sem_wait(interruptible, retval); n_waitfails = n_waitfails - retval; } proctype poster() { n_posts++; sem_post(); } #define NPROCMAX 4 init { int n_procs = NPROCMAX; do // start a non-deterministic amount of posters :: n_procs > 0 -> run poster(); n_procs--; :: 1 -> break; od; do // ditto for waiters :: n_procs > 0 -> run waiter(false); n_procs--; :: 1 -> break; od; do :: n_procs > 0 -> run waiter(true); n_procs--; :: 1 -> break; od; timeout; // wait until quiescent state assert(sem.val1 == 0 && sem.val0 == n_posts + n_waitfails - n_waits); n_procs = sem.waiters; do :: n_procs > 0 -> run poster(); n_procs--; :: else -> break; od; timeout; // wait; there should be no processes except "monitor" assert(sem.val1 == 0 && sem.val0 == n_posts + n_waitfails - n_waits); assert(sem.waiters == 0); done = true; }