mtype = {M_UP, M_DW};
#define LEN 0
chan Chan_data_down = [LEN] of {mtype};chan Chan_data_up = [LEN] of {mtype};
proctype P1 (chan Chan_data_in, Chan_data_out){ do :: Chan_data_in ? M_UP -> skip; :: Chan_data_out ! M_DW -> skip; od;};proctype P2 (chan Chan_data_in, Chan_data_out){ do :: Chan_data_in ? M_DW -> skip; :: Chan_data_out ! M_UP -> skip; od;};
init{ atomic { run P1 (Chan_data_down, Chan_data_up); run P2 (Chan_data_up, Chan_data_down); }}
Tech posts by aclassifier
Also see Designer's note page
You are at http://oyvteig.blogspot.com
Archive by month and about me: here
Last edit: 4Sept2015
Started move: September 2012
All updates at http://www.teigfam.net/oyvind/home/, but the overview is updated
Archive by month and about me: here
Last edit: 4Sept2015
Started move: September 2012
All updates at http://www.teigfam.net/oyvind/home/, but the overview is updated
Wednesday, March 18, 2009
010 - A running Promela model
Why does this code run and don't deadlock?
Subscribe to:
Post Comments (Atom)
Archive
-
►
2012
(7)
- ► 04/15 - 04/22 (1)
- ► 03/18 - 03/25 (1)
- ► 03/04 - 03/11 (1)
- ► 02/26 - 03/04 (1)
- ► 01/29 - 02/05 (2)
- ► 01/15 - 01/22 (1)
-
►
2011
(12)
- ► 12/25 - 01/01 (1)
- ► 12/18 - 12/25 (1)
- ► 11/27 - 12/04 (1)
- ► 09/25 - 10/02 (2)
- ► 08/07 - 08/14 (1)
- ► 07/17 - 07/24 (1)
- ► 06/26 - 07/03 (1)
- ► 06/12 - 06/19 (1)
- ► 03/06 - 03/13 (1)
- ► 02/06 - 02/13 (1)
- ► 01/09 - 01/16 (1)
-
►
2010
(8)
- ► 12/26 - 01/02 (1)
- ► 09/19 - 09/26 (1)
- ► 08/15 - 08/22 (1)
- ► 04/18 - 04/25 (1)
- ► 04/11 - 04/18 (1)
- ► 03/14 - 03/21 (1)
- ► 01/17 - 01/24 (2)
-
▼
2009
(13)
- ► 07/19 - 07/26 (1)
- ► 07/12 - 07/19 (1)
- ► 06/28 - 07/05 (1)
- ► 04/05 - 04/12 (1)
- ► 03/01 - 03/08 (1)
- ► 02/22 - 03/01 (1)
- ► 02/08 - 02/15 (1)
- ► 02/01 - 02/08 (1)
- ► 01/18 - 01/25 (1)
- ► 01/11 - 01/18 (2)
Popular Posts
-
iPhone movies.. The iPhone 4 produces QuickTime HD movies (.mov) that are 1280 x 720 pixels (16:9 aspect ratio). Observe that this is not th...
-
10May2021: Moved to https://www.teigfam.net/oyvind/home/older-blog-notes/
-
This note is updated at my new blog space only, blog note http://www.teigfam.net/oyvind/home/technology/050-sound-on-sound-and-picture/ ...
-
Updated 15Aug11 Intro The scope of this post is to learn how the renewed C and C++ standards may help programmers of concurrent systems ...
Øyvind Teig
- aclassifier
- Trondheim, Norway
All new blogs and new home page start at
http://www.teigfam.net/oyvind/home
Overview of old blog notes here
My technology blog was at
http://oyvteig.blogspot.com
and my handicraft blog was at
http://oyvteig-2.blogspot.com
PS: just call me "Oyvind"
All statements in an if or do have the same priority here (because there isn't an unless clause). Each transition is checked for "executability". Rendezvous communication statements (synchronous send and receives) set a local variable (rv) that represent the channel and that it is synchronous.
ReplyDeleteA wish for a send sets a "handshake" representing the wish and the channel. If a receive statement wish to receive on a channel on which a handshake is active then, provided the pattern-match fits, it will become executable (rv matches the handshake). In your example all receive-statements matches the sends, and then a non-deterministic choice is made between them. As at least one transition is possible there is no deadlock.
Remember that the semantics are defined on the global/complete state-machine, and all statements are checked for executability before one is chosen. Hope this helps.
Can you say why you originally thought that it should deadlock? is it because of the skip statements (which are redundant of course) ?
ReplyDeleteBy reading it, and mentally thinking about the two equal parts, with respect to input and output. The two parties wanting and providing the services of and to each other - symmetrically - would naturally ring a deadlock bell in my head! At the moment, being new to Promela, I in a way disagree with the non-deadlocking semantics. I haven't yet learned that behaviour! Is there too much "Promela semantics" below this code, causing it not to deadlock?
ReplyDeleteI have tried to make a summary of this at the Wikipedia Promela article (after some private communications as well). See http://en.wikipedia.org/wiki/Promela. Try Executability.
ReplyDelete