communication.xml
No OneTemporary
Actions

Subscribers

None

File Metadata

Created: Thu, Jul 9, 5:52 AM

communication.xml
View Options

	<?xml version="1.0" encoding="UTF-8"?>
	<chapter version="5.1" xmlns="http://docbook.org/ns/docbook"
	xmlns:xlink="http://www.w3.org/1999/xlink"
	xmlns:xila="http://www.w3.org/2001/XInclude/local-attributes"
	xmlns:xi="http://www.w3.org/2001/XInclude"
	xmlns:trans="http://docbook.org/ns/transclusion"
	xmlns:svg="http://www.w3.org/2000/svg"
	xmlns:m="http://www.w3.org/1998/Math/MathML"
	xmlns:html="http://www.w3.org/1999/xhtml"
	xmlns:db="http://docbook.org/ns/docbook">
	<?xxe-sn 29tvny21340 1?>

	<title><?xxe-sn 29tvny21340 2?>Communication</title>

	<para><?xxe-sn 2abbls7nbb4 2?>The chapter discusses safe usage of non-local
	variables, that is variables accessible by different components or threads
	with global variables as a particular case.</para>

	<section>
	<?xxe-sn 29xq7jt0wzk 1?>

	<title><?xxe-sn 29xq7jt0wzk 2?>Syntax</title>

	<para><?xxe-sn 29xq7jt0wzk 3?>Annotations:</para>

	<synopsis><?xxe-sn 2afyauuaxvk d?>SYNTAX:
	commop(send) (1)
	commop(receive) (2)</synopsis>

	<itemizedlist>
	<?xxe-sn 2afyauuaxvk e?>

	<listitem>
	<?xxe-sn 2afyauuaxvk f?>

	<para><?xxe-sn 2afyauuaxvk g?>annotation <code><?xxe-sn 2afyauuaxvk h?>(1)</code>
	marks <code><?xxe-sn 2afyauuaxvk i?>SEND</code> communication
	event.</para>
	</listitem>

	<listitem>
	<?xxe-sn 2afyauuaxvk j?>

	<para><?xxe-sn 2afyauuaxvk k?>annotation <code><?xxe-sn 2afyauuaxvk l?>(2)</code>
	marks <code><?xxe-sn 2afyauuaxvk m?>RECEIVE</code> communication
	event.</para>
	</listitem>
	</itemizedlist>

	<para><?xxe-sn 2afyauuaxvk n?>Specializations:</para>

	<synopsis><?xxe-sn 2afyauuaxvk o?>SYNTAX:
	commDirect
	commGuarded</synopsis>

	<para><?xxe-sn 2afyauuaxvk p?>Communication reasoning able to assign
	following specializations:</para>

	<itemizedlist>
	<?xxe-sn 2afyauuaxvk q?>

	<listitem>
	<?xxe-sn 2afyauuaxvk r?>

	<para><?xxe-sn 2afyauuaxvk s?><code><?xxe-sn 2afyauuaxvk t?>commDirect</code>
	— specialization is expected to provide direct access to raw
	variable's content.</para>
	</listitem>

	<listitem>
	<?xxe-sn 2afyauuaxvk u?>

	<para><?xxe-sn 2afyauuaxvk v?><code><?xxe-sn 2afyauuaxvk w?>commGaurded</code>
	— specialization is expected to do internal consistency checks at run
	time.</para>
	</listitem>
	</itemizedlist>
	</section>

	<section>
	<?xxe-sn 29tvny21340 3?>

	<title><?xxe-sn 29tvny21340 4?>Background</title>

	<para><?xxe-sn 29tvny21340 5?>One of the major concepts that support
	writing of safe programs is a notion of <emphasis><?xxe-sn 2abbls7nbb4 1?>immutability</emphasis>.
	Immutability tremendously simplifies many kinds of analyses; using
	immutable structures is a practical way to write multithreaded
	applications and has many other benefits beyond that. However in its most
	basic form it comes with a price of disastrous, in many cases, memory
	overhead, since property of immutability stipulates for each change of
	variable to make an independent copy of it occupying different memory
	region. Unwise using of immutable structures lead to the situation such
	that CPU is mostly occupied with unnecessary variables copying to and fro
	as well as with extensive garbage collection, irrelevant of actual
	algorithm's complexity at hand. Thus it is one of the central highlights
	of proper programming language design to provide techniques to overcome
	the shortcomings by relaxing immutability requirements keeping
	nevertheless safety benefits. There are many ways to approach the problem,
	and one such technique, namely <emphasis><?xxe-sn 2abbls7nbb4 3?>communication
	model</emphasis> is discussed next.</para>
	</section>

	<section>
	<?xxe-sn 29xq7jt0wzk 5?>

	<title><?xxe-sn 29xq7jt0wzk 6?>Communication Model</title>

	<para><?xxe-sn 29xq7jt0wzk 7?><emphasis><?xxe-sn 2abizkj6e4g 1?>Communication
	model</emphasis> is a way to capture and express what's going on with
	variables in a program as well as to define rules that describe valid
	operations over variables. Within the framework writing value to a
	variable is viewed as <emphasis><?xxe-sn 29xq7jt0wzk 8?>sending</emphasis>,
	and conversely reading variable's value is viewed as <emphasis><?xxe-sn 29xq7jt0wzk 9?>receiving</emphasis>.</para>

	<para><?xxe-sn 2abizkj6e4g 2?>Variables that are accessed from different
	components or threads are referred to as non-local variables. This chapter
	is focused on a on-local variables, global variables particularly, since
	exactly for them it's hard to manually check exhaustively where and how
	they are used in order to catch any errors. It is natural to view them as
	the means of interaction between different parts of a program, in other
	words, interaction between sender and receiver, where sender and receiver
	are different components. The same terms comprise rules that express valid
	ways of interacting. The abstraction is named <emphasis><?xxe-sn 29xq7jt0wzk a?>communication
	model</emphasis> due to similarity with the network communication.</para>

	<para><?xxe-sn 29xq7jt0wzk b?>Reasoning based on working with a
	<emphasis><?xxe-sn 2abizkj6e4g 3?>communication path</emphasis>, i.e chain
	of <emphasis><?xxe-sn 29xq7jt0wzk c?>communication events</emphasis>(e.g.
	sending/receiving) occurred during program execution.</para>

	<para><?xxe-sn 2abizkj6e4g 4?>Let's consider small example:</para>

	<programlisting><?xxe-sn 2abizkj6e4g 5?>a = init():: int; commop(send). //(1)
	b = a + 1 :: int; commop(receive). //(2)</programlisting>

	<para><?xxe-sn 2abizkj6e4g 6?>It shows computing of variable
	<code><?xxe-sn 2abizkj6e4g 7?>b</code>. Variable <code><?xxe-sn 2abizkj6e4g 8?>b</code>
	depends on <code><?xxe-sn 2abizkj6e4g 9?>a</code> so <code><?xxe-sn 2abizkj6e4g a?>a</code>
	is calculated first. Variables <code><?xxe-sn 2abizkj6e4g b?>a</code>,
	<code><?xxe-sn 2abizkj6e4g c?>b</code> are annotated with <code><?xxe-sn 2abizkj6e4g d?>comm(send)</code>
	and <code><?xxe-sn 2abizkj6e4g e?>comm(receive)</code>, denoting
	<emphasis><?xxe-sn 2abizkj6e4g f?>sending</emphasis> and
	<emphasis><?xxe-sn 2abizkj6e4g g?>receiving</emphasis> events,
	respectively. Communication path in this case is an ordered list
	<code><?xxe-sn 2abizkj6e4g h?>{<begin>, SEND, RECEIVE,
	<end>}</code> where <code><?xxe-sn 2abizkj6e4g i?><begin>,
	<end></code> — are special events that denote first and last events
	in the path, respectively.</para>

	<para><?xxe-sn 2abizkj6e4g k?>The gist of using communication model is to
	ensure that <emphasis><?xxe-sn 2abizkj6e4g l?>every sent value is properly
	received</emphasis>. It relies on the compiler to gather all possible
	communication paths in the program as an input for processing. There are
	two supported modes of reasoning:</para>

	<itemizedlist>
	<?xxe-sn 29xq7jt0wzk d?>

	<listitem>
	<?xxe-sn 29xq7jt0wzk e?>

	<para><?xxe-sn 29xq7jt0wzk f?>Validation. In this mode all
	communication paths are checked against communication rules to confirm
	that the program is valid. Otherwise compilation error is
	raised.</para>
	</listitem>

	<listitem>
	<?xxe-sn 29xq7jt0wzk g?>

	<para><?xxe-sn 29xq7jt0wzk h?>Planning. In this mode reasoning assigns
	proper implementation for variables in efforts to ensure
	validity.</para>
	</listitem>
	</itemizedlist>
	</section>

	<section>
	<?xxe-sn 29xq7jt0wzk j?>

	<title><?xxe-sn 29xq7jt0wzk k?>Validation</title>

	<para><?xxe-sn 29xq7jt0wzk l?>To perform validation, every communication
	path is checked against number of communication rules that express which
	communication path are valid. Default behaviour expressed by "every sent
	value being properly received" produce next possible cases:</para>

	<itemizedlist>
	<?xxe-sn 29xq7jt0wzk 1w?>

	<listitem>
	<?xxe-sn 29xq7jt0wzk 1x?>

	<para><?xxe-sn 29xq7jt0wzk 1y?>Valid. Path that consists of pairs of
	events <code><?xxe-sn 29xq7jt0wzk 1z?>{SEND, RECEIVE}</code> are
	<emphasis><?xxe-sn 29xq7jt0wzk 20?>valid</emphasis> meaning that each
	sent value is properly received.</para>
	</listitem>

	<listitem>
	<?xxe-sn 29xq7jt0wzk 21?>

	<para><?xxe-sn 29xq7jt0wzk 22?>Undefined and expired value. Paths that
	have parts <code><?xxe-sn 2abizkj6e4g m?>{<begin>,
	RECEIVE}</code> or <code><?xxe-sn 2abizkj6e4g n?>{RECEIVE,
	RECEIVE}</code> are invalid meaning possibly undefined value is
	received in the first case or duplication i.e. expired value is used
	in the second's one.</para>
	</listitem>

	<listitem>
	<?xxe-sn 2a3uy8rr2f4 5?>

	<para><?xxe-sn 2a3uy8rr2f4 6?>Lost value. Paths that have parts
	<code><?xxe-sn 2abizkj6e4g o?>{SEND, SEND}</code> or <code><?xxe-sn 2abizkj6e4g p?>{SEND,
	<end>}</code> indicate possibly lost change since consequent
	sender replaces value in the former case and sent value is not used at
	all in the latter case.</para>
	</listitem>
	</itemizedlist>

	<para><?xxe-sn 29xq7jt0wzk 28?>Traditional immutability validation is
	based on the idea that once valid value is valid as long it is unmodified.
	In this regards communication model can be viewed as an extension and more
	expressive tool since it also captures <emphasis><?xxe-sn 2afyauuaxvk 3?>value
	expiration</emphasis> after it was used as well as <emphasis><?xxe-sn 2afyauuaxvk 4?>value</emphasis>
	<emphasis><?xxe-sn 2afyauuaxvk 5?>loss</emphasis>, if it was not used at
	all.</para>
	</section>

	<section>
	<?xxe-sn 29xq7jt0wzk 29?>

	<title><?xxe-sn 29xq7jt0wzk 2a?>Planning</title>

	<para><?xxe-sn 2abizkj6e4g s?>Reasoning in the communication model aside
	of performing validation, also assigns appropriate specialization for
	sending and receiving operations, as appropriate. At the moment there are
	two specializations the operations are expected to support:</para>

	<itemizedlist>
	<?xxe-sn 2abizkj6e4g t?>

	<listitem>
	<?xxe-sn 2abizkj6e4g u?>

	<para><?xxe-sn 2abizkj6e4g v?>Direct. Direct specialization
	<code><?xxe-sn 2abizkj6e4g w?>commDirect</code> is expected to provide
	direct access to variable's value. This specialization is assigned in
	case of fully statically validated communication path.</para>
	</listitem>

	<listitem>
	<?xxe-sn 2abizkj6e4g x?>

	<para><?xxe-sn 2abizkj6e4g y?>Guarded. In case if there are possible
	communication path inconsistencies that can not be completely ruled
	out at compile time, checking logic should be embedded into compiled
	code. Specialization <code><?xxe-sn 2abizkj6e4g z?>commGaurded</code>
	is expected to hold variable state and check usage consistency.</para>
	</listitem>
	</itemizedlist>
	</section>

	<section>
	<?xxe-sn 2a3uy8rr2f4 8?>

	<title><?xxe-sn 2a3uy8rr2f4 9?>Planning Horizon</title>

	<para><?xxe-sn 2a3uy8rr2f4 a?>Reasoning implements algorithm that is
	bounded by the maximal path length it can process. The parameter is called
	<emphasis><?xxe-sn 2a3uy8rr2f4 b?>planning horizon</emphasis>. Any
	variable that it can not check due to exceedingly large path's length is
	assigned default implementation <code><?xxe-sn 2abizkj6e4g 10?>commGaurded</code>
	that performs necessary checks during runtime. Thus the parameter
	regulates trade off between static analysis extensiveness and runtime
	checks overhead.</para>
	</section>

	<section>
	<?xxe-sn 2a7t1hxqqyo 1?>

	<title><?xxe-sn 2a7t1hxqqyo 2?>Example: Direct Implementation</title>

	<programlisting xml:id="DirImpl_1"><?xxe-sn 2a7t1hxqqyo 3?>name="tests/effects-communication.cpp: Doc_DirImpl", lines=15
	import raw("scripts/dfa/propagation.lp").
	import raw("scripts/dfa/polymorphism.lp").
	import raw("scripts/effects-communication/communication.lp").
	import raw("scripts/effects-communication/config.lp").

	CommDirect = type {
	value:: int
	}.

	guard:: commDirect {
	init = function::CommDirect
	{
	{value = 0}
	}

	read = function(vault1:: CommDirect):: int
	{
	(vault1:: *;commop(receive))["value"]
	}

	write = function(vault2:: CommDirect, valueNew:: int)::CommDirect
	{
	(vault2:: *; dfa_pseudo(vault2)) + {value = valueNew}:: int; commop(send); dfa_uppy(vault2)
	}
	}

	main = function::int; entry {
	x1 = init()::*; dfa_polym(ret).
	x2 = write(x1, 1)::*; dfa_polym(arg).
	val = read(x2)::int; dfa_polym(arg).
	val
	}</programlisting>

	<para><?xxe-sn 2a7t1hxqqyo 4?>In this example, basic workflow is presented
	in <code><?xxe-sn 2afyauuaxvk 1?>main</code> — the function
	<code><?xxe-sn 2a7t1hxqqyo 5?>write(x1, 1)</code> is invoked following by
	invocation of <code><?xxe-sn 2a7t1hxqqyo 6?>read(x2)</code>. Functions
	<code><?xxe-sn 2afyauuaxvk 9?>write()</code> and <code><?xxe-sn 2afyauuaxvk a?>read()</code>
	are annotated with <code><?xxe-sn 2afyauuaxvk b?>commop(send)</code> and
	<code><?xxe-sn 2afyauuaxvk c?>commop(receive)</code> respectively in order
	to enable communication reasoning. Analyzer gathers and validates observed
	communication path and since there is no ambiguity, it's possible to
	assign specialization <code><?xxe-sn 2a7t1hxqqyo 7?>CommDirect</code>
	allowing direct access to the variables avoiding any additional overhead.
	Note, there are no any other specializations defined and if reasoning was
	not enable to conclude that it is the case the compilation error would be
	raised.</para>
	</section>

	<section>
	<?xxe-sn 2a7t1hxqqyo 9?>

	<title><?xxe-sn 2a7t1hxqqyo a?>Example: Guarded Implementation</title>

	<programlisting xml:id="GuardedImpl_1"><?xxe-sn 2a7t1hxqqyo b?>name="tests/effects-communication.cpp: Doc_GuardedImpl", lines=15
	import raw ("scripts/effects-communication/communication.lp").
	import raw ("scripts/dfa/propagation.lp").
	import raw ("scripts/dfa/polymorphism.lp").
	import raw ("scripts/effects-communication/config.lp").

	CommState = type variant{Invalid, Valid, Outdated}.

	CommDirect = type {
	value:: int
	}.

	CommGuarded = type {
	value:: int,
	state:: CommState
	}.

	guard:: commDirect {
	init=function::CommDirect{
	{value = 0}
	}

	read= function(vault1:: CommDirect):: int{
	(vault1::CommDirect; commop(receive))["value"]
	}

	write= function(vault2:: CommDirect, valueNew1:: int)::CommDirect{
	(vault2::CommDirect;dfa_pseudo(vault2)) + {value = valueNew1}:: int; commop(send); dfa_uppy(vault2)
	}
	}

	errorRead = function:: int { -1 }

	errorWrite = function:: CommGuarded{
	{
	value = -1,
	state = Invalid()
	}
	}

	guard:: commGuarded{
	init=function::CommGuarded{
	{
	value = 0,
	state = Invalid()
	}
	}

	read=function(vault3:: CommGuarded):: int {
	switch variant (vault3["state"]->whatever::CommState;commop(receive)):: int
	case (Invalid) { errorRead() }
	case (Outdated) { errorRead() }
	case (Valid) { vault3["value"] }
	}

	write=function(vault4:: CommGuarded, valueNew2:: int)::CommGuarded{
	switch variant (vault4["state"]->whatever::CommState;commop(send); dfa_pseudo(vault4))::int
	case (Invalid) {
	{value = valueNew2, state = Valid()}:: CommGuarded; dfa_uppy(vault4)
	}

	case (Outdated) {
	{value = valueNew2, state = Valid()}:: CommGuarded; dfa_uppy(vault4)
	}

	case (Valid) { errorWrite():: CommGuarded; dfa_uppy(vault4) }
	}
	}

	main=function(cmd:: num)::int; entry {
	x1 = init():: *; dfa_polym(ret).
	x2 = write(x1, 1)::*; dfa_polym(arg).

	x3 = if (cmd > 0)::int {
	y = read(x2):: int; dfa_polym(arg).
	y

	} else {
	z = write(x2, 2)::*; dfa_polym(arg).
	a = read(z):: int; dfa_polym(arg).
	a
	}.

	x3
	}</programlisting>

	<para><?xxe-sn 2a7t1hxqqyo d?>Here example of slightly more complicated
	workflow. Function <code><?xxe-sn 2afyauuaxvk 2?>main</code> contains
	branching that depends on argument known at run time only. Analyzer is
	presented with two possible communication paths and one of them(false
	branch) leads to a possibly lost value for it contains two consequent
	<code><?xxe-sn 2afyauuaxvk 6?>SEND</code> events. In this situation the
	analyzer unable to statically validate correctness and assigns
	specialization <code><?xxe-sn 2afyauuaxvk 7?>commGuarded</code> to embed
	checking logic into compiled code as an intermediary layer between
	variable's content and client's code. Implementation <code><?xxe-sn 2afyauuaxvk 8?>commGuarded</code>
	along with a variable access also tracks the variable status and returns
	error if the value is inconsistent.</para>
	</section>
	</chapter>
	<?xxe-revisions
	#1 2019-03-07T18:27:57Z pgess
	?>

communication.xmlNo OneTemporaryActions

File Metadata

communication.xmlView Options

Event Timeline

communication.xml
No OneTemporary
Actions

communication.xml
View Options