Skip to Content.
Sympa Menu

k-user - Re: [K-user] How to check if all threads have finished execution

k-user AT lists.cs.illinois.edu

Subject: K-user mailing list

List archive

Re: [K-user] How to check if all threads have finished execution


Chronological Thread 
  • From: Traian Florin Şerbănuţă <traian.serbanuta AT fmi.unibuc.ro>
  • To: Omar Duhaiby <3omarz AT gmail.com>
  • Cc: "k-user AT cs.uiuc.edu" <k-user AT cs.uiuc.edu>
  • Subject: Re: [K-user] How to check if all threads have finished execution
  • Date: Thu, 16 Oct 2014 11:48:10 +0300
  • List-archive: <http://lists.cs.uiuc.edu/pipermail/k-user/>
  • List-id: <k-user.cs.uiuc.edu>

What one usually does (see, e.g., SIMPLE) is to erase threads which have nothing in their <k> cell, with rules like

rule <thread>...
  <k> .K </k>
...</thread> => .

This keeps the thread space clean and also makes rewriting faster.  If doing so, then you can check whether there is only one thread left by matching only one thread in the threads cell (it is always good to group similar cells like thread into a single cell, like threads).

rule <threads> <thread>... <k> K => enter_single_mode(K) </k> ...</thread> </threads>

Hope this helps,
Traian


2014-10-16 10:59 GMT+03:00 Omar Duhaiby <3omarz AT gmail.com>:
Hello,

I have one thread that is always active. The problem is that the program will not halt as long as that thread is active. It is a counter of transitions made during execution. My question is:

1- Is there a better way to count the number of transitions of a certain thread or the whole program?
2- How do I check if all other threads have nothing in their k cells? because '_' includes '.'
    I tried doing this:
    rule (some rewrite)
        <thread>...
          <k> Code:K </k>
        ...</thread>
    when Code =/=K .K

I really don't know what I'm doing here. I was just trying my luck. The idea is that this rule should only work if there is at least one thread that has something in its k cell. Question: will this match against the thread that I'm rewriting?
If all fails, I can always make a new cell to act as a flag, call it "isActive". Any ideas?

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





Archive powered by MHonArc 2.6.16.

Top of Page