{"id":524,"date":"2007-10-04T21:12:34","date_gmt":"2007-10-04T21:12:34","guid":{"rendered":"http:\/\/scientopia.org\/blogs\/goodmath\/2007\/10\/04\/counted-petri-nets-and-useless-protocol-specification-tools\/"},"modified":"2007-10-04T21:12:34","modified_gmt":"2007-10-04T21:12:34","slug":"counted-petri-nets-and-useless-protocol-specification-tools","status":"publish","type":"post","link":"http:\/\/www.goodmath.org\/blog\/2007\/10\/04\/counted-petri-nets-and-useless-protocol-specification-tools\/","title":{"rendered":"Counted Petri Nets, and Useless Protocol Specification Tools"},"content":{"rendered":"

There’s one variant of Petri nets, called counted<\/em> Petri nets, which I’m fond of for personal reasons. As Petri net variants go, it’s a sort of sloppy but simple one, but as I said, I’m fond of it.<\/p>\n

As a warning, there’s a bit of a diatribe beneath the fold, as I explain why I know about this obscure, strange Petri net variant.<\/p>\n

<\/p>\n

My first project in grad school involved building a simulator for a network protocol specification language called Estelle.<\/a> Estelle is, as I like to describe it, a formal specification language with absolutely no useful formal qualities.<\/p>\n

The problem with Estelle is that it’s based on something called augmented heirarchical communicating finite state machines. Communicating FSMs are fine; heirarchical FSMs are fine. They’re not my favorite model, but they’re useful, valid techniques for describing things.<\/p>\n

Where Estelle got into trouble was the “augmented” part. What that meant is that
\neach FSM had a bunch of data associated with it, and each transition had a set of guard conditions and effect code written in Pascal. So a state transition could run an arbitrary Pascal program that altered the state of the FSM without changing the visible FSM state; and that change could affect the guard conditions determining what transitions could occur later. So every Estelle transition is basically unlimited in its effects. Any analysis that tried to answer questions about a specification that used this capability generally reduced to the halting problem; but you really needed to use it to represent the state
\ninvolved in communication protocols!<\/p>\n

Anyway, I got roped into this, and I was supposed to port a huge Smalltalk simulator of Estelle to C. Only I’d never really used Smalltalk. I knew the theory of it, but I’d never had access to a real Smalltalk interpreter. So as a way to learn Smalltalk, and to get into the swing of this protocol specification stuff, I wrote a simple counted Petri net simulator.<\/p>\n

Interestingly, I can’t find anything about counted Petri nets on the internet, so I assume they died an ignomious death. I’ll revive them for a brief moment, because they’re an interesting simple example of how to extend Petri nets. The extension is very simple and very minimal, and has some theoretical awkwardness, but it’s useful for expressing certain kinds of fairly common concurrency patterns.<\/p>\n

All that you do when you extend to counted Petri nets is to add an integer to each transition. The transition can fire not when all of its input edges have tokens waiting, but when some collection of tokens from the input arcs can provide enough tokens. The counts on the edges become a bound<\/em> on the maximum number of tokens that can move across the arc.<\/p>\n

What this is useful for is things like the worker pool<\/em> pattern. In this kind of concurrency, you have one main thread, and many workers. The main thread creates tasks which are put into a pool. The workers each grab tasks from the pool and perform the tasks, until no tasks are left in the pool. The reason for using a pool is load balancing: the tasks take different amounts of time to complete, and you don’t know which tasks are going to take longer. So each of the workers grabs a random task from the pool, and runs it. If it’s a fast one, it finishes it quickly, and then grabs another. This means that the processors will all be busy processing tasks for roughly the same amount of time, but they’ll end up processing different numbers of tasks. The synchronization scheme for this is for the main thread to set up the task pool, and then wait after putting the tasks into the pool, the main thread waits until all of
\nthe tasks are complete.<\/p>\n

\"worker-pool-petri.png\"<\/p>\n

How would you represent a worker pool with a Petri net? You have a pool of workers thread, all of which are basically equivalent. The main thread puts tokens (representing the tasks) into a place representing the task pool. The task pool has a collection of out edges, one for each thread, which carry the task tokens to a subnet representing the task threads. The worker threads each have a place at the
\nend where they deposit tokens for completed tasks. The main thread waits on a transition which doesn’t get a token until all of the tasks are completed. That token comes from a place which gets its<\/em> token only when all of the tasks are complete. Since the different tasks will have performed different numbers
\nof tasks, we use a transition that fires when all of the tasks are complete. A very simple example of this, with two worker tasks is in the image to the right. The main thread is colored green; the places and transitions that control the synchronization of worker threads are red, and the worker threads themselves are blue.<\/p>\n

The counted net is a strange sort of hybrid. It’s basically adding a primitive sort of counting to the nets, which is useful. But it does it in a way which is extremely limited. For example, in a real task pool scenario, you wouldn’t know<\/em> how many tasks were going to be dispatched to the pool; but the transition needs to be marked with a specific value. So for the purposes of the net, you pretend to know.<\/p>\n

As I mentioned, this adds a bit of theoretical awkwardness. One of the great things about Petri nets is that they’ve got a very strong notion of synchronization. But with counted nets, that gets weakened. It doesn’t show in this example – but for non-trivial nets, you can get cases where things get tangled – where you want at least 1 token from each of some group of places, but you can’t guarantee that properly
\nwithout adding a bunch of extra layers of places and transitions – which messes up the simplicity and clarity which is the main reason for using Petri nets.<\/p>\n

Next week, I’ll describe colored<\/em> Petri nets, which are a much stronger, much cleaner way of extending the capability of Petri nets. The basic idea is that tokens can carry information, and lamba calculus functions can be associated with transitions.<\/p>\n","protected":false},"excerpt":{"rendered":"

There’s one variant of Petri nets, called counted Petri nets, which I’m fond of for personal reasons. As Petri net variants go, it’s a sort of sloppy but simple one, but as I said, I’m fond of it. As a warning, there’s a bit of a diatribe beneath the fold, as I explain why I […]<\/p>\n","protected":false},"author":1,"featured_media":0,"comment_status":"open","ping_status":"open","sticky":false,"template":"","format":"standard","meta":{"jetpack_post_was_ever_published":false,"_jetpack_newsletter_access":"","_jetpack_dont_email_post_to_subs":false,"_jetpack_newsletter_tier_id":0,"_jetpack_memberships_contains_paywalled_content":false,"_jetpack_memberships_contains_paid_content":false,"footnotes":"","jetpack_publicize_message":"","jetpack_publicize_feature_enabled":true,"jetpack_social_post_already_shared":false,"jetpack_social_options":{"image_generator_settings":{"template":"highway","default_image_id":0,"font":"","enabled":false},"version":2}},"categories":[25,42],"tags":[],"class_list":["post-524","post","type-post","status-publish","format-standard","hentry","category-graph-theory","category-networks"],"jetpack_publicize_connections":[],"jetpack_featured_media_url":"","jetpack_shortlink":"https:\/\/wp.me\/p4lzZS-8s","jetpack_sharing_enabled":true,"jetpack_likes_enabled":true,"_links":{"self":[{"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/posts\/524","targetHints":{"allow":["GET"]}}],"collection":[{"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/users\/1"}],"replies":[{"embeddable":true,"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/comments?post=524"}],"version-history":[{"count":0,"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/posts\/524\/revisions"}],"wp:attachment":[{"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/media?parent=524"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/categories?post=524"},{"taxonomy":"post_tag","embeddable":true,"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/tags?post=524"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}