communication.xml
No OneTemporary
Actions

Subscribers

None

File Metadata

Created: Thu, Jul 9, 8:29 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 is able to assign
	the 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?>commGuarded</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 the price of a disastrous, in many cases, memory
	overhead, since the property of immutability implies that with each change
	of a variable an independent copy of it shall be made, occupying a
	different memory region. Unwise use of immutable structures would lead to
	a situation where 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 one of the
	central points of a proper programming language design is enabling the
	techniques that would help to overcome the shortcomings by relaxing the
	immutability requirements while keeping the 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 is going on with
	variables in a program as well as to define rules that describe valid
	operations over variables. Within this framework, writing a value to a
	variable is viewed as <emphasis><?xxe-sn 29xq7jt0wzk 8?>sending</emphasis>,
	while reading a 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 non-local variables, the global ones particularly, since it
	is the very type of variables for which it is difficult to perform a
	manual exhaustive check and find out where and how they are used in order
	to catch any errors. It is natural to view them as the means of an
	interaction between different parts of a program, in other words, an
	interaction between a sender and receiver, where such 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 a
	chain of <emphasis><?xxe-sn 29xq7jt0wzk c?>communication events</emphasis>
	(e.g. sending/receiving) that occur during program execution.</para>

	<para><?xxe-sn 2abizkj6e4g 4?>Let's consider a 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 the 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> and
	<end></code> are special events that denote the 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 a 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 define which
	communication paths are valid. Default behaviour expressed by the "every
	sent value being properly received" presumption results in the next
	possible cases:</para>

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

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

	<para><?xxe-sn 29xq7jt0wzk 1y?>Valid. Paths that consist 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 was properly received.</para>
	</listitem>

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

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

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

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

	<remark><?xxe-sn 2eeqemlan74 pu35zrt1abya?>Не вполне понятен смысл
	фразы "consequent sender", и перед ней нужен артикль</remark>
	</listitem>
	</itemizedlist>

	<para><?xxe-sn 29xq7jt0wzk 28?>Traditional immutability validation is
	based on a concept that a valid value shall remain valid as long as it was
	not modified. In this regard the 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?>Aside of performing validation, reasoning in
	the communication model also assigns appropriate specialization to 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 a variable's value. This specialization is assigned
	in case of a fully statically validated communication path.</para>
	</listitem>

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

	<para><?xxe-sn 2abizkj6e4g y?>Guarded. In case there are possible
	communication path inconsistencies that cannot 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 track a variable's state in order to be able to check
	usage consistency.</para>

	<remark><?xxe-sn 2eeqemlan74 pu35zrt1abyb?>"hold variable state" - ?
	Удерживать переменную в каком-либо состоянии? Зафиксировать ее
	состояние? Тогда может лучше "hold the [current] state of a variable"?
	Или даже seize?</remark>
	</listitem>
	</itemizedlist>
	</section>

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

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

	<para><?xxe-sn 2a3uy8rr2f4 a?>Reasoning implements an 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 cannot 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
	establishes a trade-off between the static analysis extensiveness and the
	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 is 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 other specializations defined, and if reasoning was not
	able to conclude direct access specialization, then the compilation error
	would be raised.</para>

	<remark><?xxe-sn 2eeqemlan74 pu35zrt1abyc?>"is invoked following by
	invocation" - тут из-за грамматики не ясно, что за чем следует. Предлагаю
	заменить на "is invoked after the invocation of...", или на "is invoked
	following the invocation of..."</remark>

	<remark><?xxe-sn 2eeqemlan74 pu35zrt1abyd?></remark>

	<remark><?xxe-sn 2eeqemlan74 pu35zrt1abye?>\| "if reasoning was not able to
	conclude that it was the case" - лучше уточнить что подразумевается под
	словами "that it was the case" - "расшифровать", т.к. мне например не
	понятно</remark>
	</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 is an example of a slightly more
	complicated workflow. Function <code><?xxe-sn 2afyauuaxvk 2?>main</code>
	contains branching that depends on an argument known at run time only.
	Analyzer is presented with two possible communication paths, one of which
	(the false branch) leads to a possibly lost value for it contains two
	consequent <code><?xxe-sn 2afyauuaxvk 6?>SEND</code> events. In this
	situation analyzer is 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
	the variable's content and the client's code. Implementation
	<code><?xxe-sn 2afyauuaxvk 8?>commGuarded</code> besides accessing to a
	variable's value also tracks the variable's status and will return error
	if the value is inconsistent.</para>

	<remark><?xxe-sn 2eeqemlan74 pu35zrt1abyf?>"along with a variable access"
	- ? Если буквально переводить, получается "вместе с переменным доступом".
	Нужен или апостроф после variable, или как-то перефразировать.</remark>
	</section>
	</chapter>
	<?xxe-revisions
	#4 2019-05-20T09:53:54Z pgess
	#3 2019-04-30T23:02:25Z Администратор
	1sPEAAABgYxnAHuBjAYAA0EwcmVyc6gYEwQBAUMJQ4IpYwlTEmOYMGMEUwcTBAECMwhTBlMuQwQz
	jhpTE2MFEwUTB1MLQ5ceMxRTBEMHM55BYxxjgzgAlhLDR5IYqxOLE4JIP5g4hnw4lmAOtlMxjxeH
	B7lDhDGLepk/mzgdmVuXRYIlgRo=

	#2 2019-04-29T21:50:35Z Администратор
	1sPEAAABgYwHAINs/zEAFYINgUJvZHVjLidpZGVhdW5yZWdzICdtKHNzuW4TCkMEUw5jBTMEYyZT
	LQEEY4EVMw0TBUOBH1MUUwoTIGNcY4EXQwczElMFUxwzCxMEAQFDDmMFUwRjB2MGpHMKY2mDIlOB
	ExMFIwQTCDMKMwRjDjMsgwwzIGM/QwQBBFMGUwRDDRMFUwxjBgECMxhjBFODSEMKgxwzH1MoQwQz
	gm5TPWOBFTMGEweDGzMZIwUzgWmDDJMQUx8zClNxMwhjgS2DBTMFQ4FBqr0BAVMMQwZjHDMHMwgT
	CHMKgykTFUOMViMGMx4BAVOBM2MEEwYzF4MFUxVDBTMWQwdjBFMGQyqDkxhjCzN9Q1uDBRMKAQJT
	gRJzBBMFUwRDgURDF1OBBmMMMwalQydjFgCdC4Rrk0yhF45hhFEqRIEWpQERjU6MOokcgV5ggV6B
	LIZ1GB6nKxTFH5MHii0gmCW7FWaBD6R2gkuMX4Eog3+lZSOcgWGCCLg4vWpCDYRVHJx6GpJVH4R4
	iYNJG5ByK4JwP7oKmgGZgTqLJh2cfZ5ytjWUC40GfLChOIE2rBuBTgeiaRaKEIoBlRC7x4M/qR6f
	T4xdIIEHlBUynh2EVxiIZpk/GRXHkx4NgQCemCdvtZMso0WBHoFIG4EIEfpmDIJq
	#1 2019-03-07T18:27:57Z pgess
	1sPEAAAB/zEAgm7+QQAkgUCBAnN0aXB0byBtYWtoaWdobnRoZWwnZWNvbmEgZXhhY2hhcmxseXOF
	DxOHP0MPU4MJIw9jhDtDJlMEUwczMkMZAQRjBVMGUw8jCQEGQxxjCjMiIwRDGGMIMwQzClMGEwRT
	gS0jBkMT3WMFgwZjHRMLYwxDKFMaYwi7uBMEM4EbIwQzggYBAVN6AQFjChMJM1lDBAEDEwQjBCME
	kwQzggIBAhMUQxFTCjMK6DMEMwVTBQEDEwVDBgEBYwdTCwECM2ZDQpMUEwRTGEODEFNMYx4zBDNP
	U4dgQw0TCUMEMwRTGzOEekPJKQCFEIdCE78xgxiEPIQLLAk2k1eMSiuWKBgrDLBlJB6KSwqDSYRR
	ELIqgS2TYoxapCWOQS0cLCCfPpowhC0Qn3uBIIIIfJITFoUkCbwTvTFtnwuEPFoWgjGRWKgFgUeZ
	Po4/k1ixOwYeaaSGfF8dgxJNh0MgUZJnihaEDJ5IoksfhHw=
	?>

communication.xmlNo OneTemporaryActions

File Metadata

communication.xmlView Options

Event Timeline

communication.xml
No OneTemporary
Actions

communication.xml
View Options