k-user AT lists.cs.illinois.edu

Subject: K-user mailing list

List archive

Re: [K-user] condition: all threads are stuck

From: Dwight Guth <dwight.guth AT runtimeverification.com>
To: Omar Duhaiby <3omarz AT gmail.com>
Cc: "k-user AT cs.uiuc.edu" <k-user AT cs.uiuc.edu>
Subject: Re: [K-user] condition: all threads are stuck
Date: Wed, 19 Nov 2014 10:04:31 -0600
List-archive: <http://lists.cs.uiuc.edu/pipermail/k-user/>
List-id: <k-user.cs.uiuc.edu>

This is not quite like you have described, but if you are interested in causing all threads to wait until a particular moment and then release some of them, you might look at the code for "barrier" in the definition "agent" in the samples directory.

On Sun, Nov 16, 2014 at 6:29 AM, Omar Duhaiby <3omarz AT gmail.com> wrote:

Can I make a rule match on the condition that all threads are stuck? I'm trying to do some kind of synchronization.

_______________________________________________
k-user mailing list
k-user AT cs.uiuc.edu
http://lists.cs.uiuc.edu/mailman/listinfo/k-user

[K-user] condition: all threads are stuck, Omar Duhaiby, 11/16/2014
- Re: [K-user] condition: all threads are stuck, Dwight Guth, 11/19/2014