<html>
<head>
<meta http-equiv="content-type" content="text/html; charset=utf-8">
</head>
<body bgcolor="#FFFFFF" text="#000000">
<p><br>
</p>
<div class="moz-forward-container"><br>
<br>
-------- Forwarded Message --------
<table class="moz-email-headers-table" border="0" cellpadding="0"
cellspacing="0">
<tbody>
<tr>
<th align="RIGHT" nowrap="nowrap" valign="BASELINE">Subject:
</th>
<td>Re: [P4-discuss] Question regarding semantics of actions
in P4-14 (v1.0.3)</td>
</tr>
<tr>
<th align="RIGHT" nowrap="nowrap" valign="BASELINE">Date: </th>
<td>Thu, 19 Jan 2017 02:15:10 -0800</td>
</tr>
<tr>
<th align="RIGHT" nowrap="nowrap" valign="BASELINE">From: </th>
<td>Nate Foster <a class="moz-txt-link-rfc2396E" href="mailto:jnfoster@cs.cornell.edu"><jnfoster@cs.cornell.edu></a></td>
</tr>
<tr>
<th align="RIGHT" nowrap="nowrap" valign="BASELINE">To: </th>
<td>Ali Kheradmand <a class="moz-txt-link-rfc2396E" href="mailto:a.i.kheradmand@gmail.com"><a.i.kheradmand@gmail.com></a>, Nikolaj
Bjorner <a class="moz-txt-link-rfc2396E" href="mailto:nbjorner@microsoft.com"><nbjorner@microsoft.com></a></td>
</tr>
<tr>
<th align="RIGHT" nowrap="nowrap" valign="BASELINE">CC: </th>
<td>Grigore Rosu <a class="moz-txt-link-rfc2396E" href="mailto:grigore.rosu@gmail.com"><grigore.rosu@gmail.com></a>,
<a class="moz-txt-link-abbreviated" href="mailto:p4-discuss@lists.p4.org">p4-discuss@lists.p4.org</a></td>
</tr>
</tbody>
</table>
<br>
<br>
<div dir="ltr">
<div>
<div>Hi Ali,</div>
<div><br>
</div>
<div>It's almost like one needs to formalize the semantics to
make sense of this! ;-) <br>
</div>
</div>
<div><br>
</div>
<div>I wasn't involved with drafting the P4-14 spec so I could
be wrong, but based on the informal text, I believe the
intention is that the order of the statements is ignored, but
the primitive instructions are executed with something akin to
"true concurrency" and what Lamport calls "regular" in his
classic work on semantics of registers. That is, after
executing a the field h.a would either have the value 1 or 2,
but not some other value (which weaker notions like "safe
registers" allow, due to hazards that may occur when shared
memory is written by two different threads simultaneously).<br>
<div><br>
</div>
<div>The way I would model this in an operational semantics is
to (i) copy the old state before evaluating the primitives
in the action body and (ii) define a merge operation that
takes the updated states produced by evaluating the
primitives and (non-deterministically) merges them to get a
new state. </div>
<div><br>
</div>
<div>Maybe Nikolaj can weigh in on how P4-NoD handled this
issue?</div>
</div>
<div><a moz-do-not-send="true"
href="https://www.microsoft.com/en-us/research/wp-content/uploads/2016/09/p4nod.pdf">https://www.microsoft.com/en-us/research/wp-content/uploads/2016/09/p4nod.pdf</a><br>
</div>
<div><br>
</div>
<div>Cheers,</div>
<div>-N</div>
</div>
<div class="gmail_extra"><br>
<div class="gmail_quote">On Wed, Jan 18, 2017 at 11:59 AM, Ali
Kheradmand <span dir="ltr"><<a moz-do-not-send="true"
href="mailto:a.i.kheradmand@gmail.com" target="_blank">a.i.kheradmand@gmail.com</a>></span>
wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0
.8ex;border-left:1px #ccc solid;padding-left:1ex">
<div dir="ltr">
<div>Hi,</div>
<div><br>
</div>
<div>In the language specification version 1.0.3, section
9.2.1 it is stated that “P4 assumes parallel semantics
for the application of all the primitive actions
executing as a result of a match in a given table.” It
also mentions that “With parallel semantics, […] actions
are started at the same time”. </div>
<div><br>
</div>
<div>I was wondering whether it means that the order of
actions are not important at all or not. If the order is
ignored, I what happens if two primitive actions that
are executed as a result of a match have overlapping
effects, for example:</div>
<div>action a ( ) {</div>
<div> modify_field(h.a, 1);</div>
<div> modify_field(h.a, 2);</div>
<div>}</div>
<div><br>
</div>
<div>If the order is important, how exactly it relates to
the parallel semantics? </div>
<div><br>
</div>
<div>Regards,</div>
<div>Ali</div>
</div>
</blockquote>
</div>
<br>
</div>
</div>
<br /><br />
<hr style='border:none; color:#909090; background-color:#B0B0B0; height: 1px; width: 99%;' />
<table style='border-collapse:collapse;border:none;'>
<tr>
<td style='border:none;padding:0px 15px 0px 8px'>
<a href="https://www.avast.com/antivirus">
<img border=0 src="http://static.avast.com/emails/avast-mail-stamp.png" alt="Avast logo" />
</a>
</td>
<td>
<p style='color:#3d4d5a; font-family:"Calibri","Verdana","Arial","Helvetica"; font-size:12pt;'>
Ezt az e-mailt az Avast víruskereső szoftver átvizsgálta.
<br><a href="https://www.avast.com/antivirus">www.avast.com</a>
</p>
</td>
</tr>
</table>
<br />
</body>
</html>