diff --git a/config/default.json b/config/default.json index e2db4c2..baf997f 100644 --- a/config/default.json +++ b/config/default.json @@ -1,74 +1,74 @@ { "containers": { "id": { "implementations": "containers_impl", "linkedlist": "linkedlist" }, "impl": { "solid": "solid", "onthefly": "on_the_fly" } }, "logging": { "id": "logging" }, "function-entry": "entry", "transcend": { "bindings" : { "variable": "bind", "function": "bind_func", "scope": "bind_scope", "function_demand" : "bind_function_demand", "scope_decision": "bind_scope_decision" }, "context" : { "decisions":{ "dependent": "resolution_dependency" } }, "nonevalue": "nonevalue", "ret": { "symbol": "retv", "tag": "ret" } }, "tests": { "template": "troubleshooting", "templates": { - "troubleshooting":"ASTCorrespondence.Doc_*:Virtualization.Doc_*:Exploitation.Doc_*", - "documentation":"Modules.Doc_*:Interpretation.Doc_*:AST.Doc_*:Loop.Doc_*:LateReasoning.Doc_*:Latex.Doc_*:Polymorphs.Doc_*:Transcend.Doc_*:ASTCorrespondence.Doc_*:Virtualization.Doc_*:Exploitation.Doc_*", + "troubleshooting":"Virtualization.Doc_*:Exploitation.Doc_*:Communication.Doc_*", + "documentation":"Modules.Doc_*:Interpretation.Doc_*:AST.Doc_*:Loop.Doc_*:LateReasoning.Doc_*:Latex.Doc_*:Polymorphs.Doc_*:Transcend.Doc_*:ASTCorrespondence.Doc_*:Virtualization.Doc_*:Exploitation.Doc_*:Communication.Doc_*", "default": "*", "ast": "AST.*", "effects": "Effects.*", "basic": "Attachments.*", "compilation": "Compilation.*", "communication": "Communication.*", "cfa": "CFA.*", "containers": "Containers.*", "dfa": "DFA.*", "diagnostic": "Diagnostic.*", "dsl": "Association.*:Interpretation.*", "exploitation": "Exploitation.*", "ExpressionSerializer": "ExpressionSerializer.*", "externc": "InterfaceExternC.*", "loops": "Loop.*", "latereasoning": "LateReasoning.*", "latex": "Latex.*", "modules": "Modules.*", "polymorphs": "Polymorphs.*", "intrinsic-query": "Types.SlaveTypes*:Association.TypedQuery*", "types": "Types.*", "virtualization": "Virtualization.*", "vendorsAPI/clang": "ClangAPI.*", "vendorsAPI/xml2": "libxml2.*" } } } diff --git a/cpp/tests/effects-communication.cpp b/cpp/tests/effects-communication.cpp index 652b88b..b9193f7 100644 --- a/cpp/tests/effects-communication.cpp +++ b/cpp/tests/effects-communication.cpp @@ -1,73 +1,89 @@ /* Any copyright is dedicated to the Public Domain. * http://creativecommons.org/publicdomain/zero/1.0/ * * communication.cpp * * Author: pgess * Created on October 14, 2017, 5:24 PM */ #include "xreatemanager.h" +#include "supplemental/docutils.h" + #include "gtest/gtest.h" + using namespace xreate; +using namespace std; TEST(Communication, ast_Basic1){ FILE* script = fopen("scripts/effects-communication/example1-wr.xreate", "r"); std::unique_ptr program(XreateManager::prepare(script)); ASSERT_TRUE(true); fclose(script); } TEST(Communication, analysis_Basic1){ FILE* script = fopen("scripts/effects-communication/example1-wr.xreate", "r"); std::unique_ptr program(details::tier1::XreateManager::prepare(script)); fclose(script); program->analyse(); ASSERT_TRUE(true); } TEST(Communication, full_Basic1){ FILE* script = fopen("scripts/effects-communication/example1-wr.xreate", "r"); std::unique_ptr program(XreateManager::prepare(script)); fclose(script); int (*programEntry)() = (int (*)())program->run(); int result = programEntry(); ASSERT_EQ(1, result); } TEST(Communication, full_Basic2){ FILE* script = fopen("scripts/effects-communication/example2-wr.xreate", "r"); std::unique_ptr program(XreateManager::prepare(script)); fclose(script); int (*programEntry)() = (int (*)())program->run(); int result = programEntry(); ASSERT_EQ(1, result); } TEST(Communication, analysis_Weak1){ FILE* script = fopen("scripts/effects-communication/example3-wrwr.xreate", "r"); std::unique_ptr program(details::tier1::XreateManager::prepare(script)); fclose(script); program->analyse(); ASSERT_TRUE(true); } TEST(Communication, full_Weak1){ FILE* script = fopen("scripts/effects-communication/example3-wrwr.xreate", "r"); std::unique_ptr program(XreateManager::prepare(script)); fclose(script); int (*programEntry)(int) = (int (*)(int))program->run(); ASSERT_EQ(1, programEntry(1)); ASSERT_EQ(-1, programEntry(0)); +} + +TEST(Communication, Doc_DirImpl){ + string example = getDocumentationExampleById("documentation/communication.xml", "DirImpl_1"); + XreateManager* xreate = XreateManager::prepare(move(example)); + xreate->run(); +} + +TEST(Communication, Doc_GuardedImpl){ + string example = getDocumentationExampleById("documentation/communication.xml", "GuardedImpl_1"); + XreateManager* xreate = XreateManager::prepare(move(example)); + xreate->run(); } \ No newline at end of file diff --git a/documentation-api/communicaton.graphml b/documentation-api/communicaton.graphml new file mode 100644 index 0000000..a1a0b9d --- /dev/null +++ b/documentation-api/communicaton.graphml @@ -0,0 +1,447 @@ + + + + + + + + + + + + + + + + + + + + + + + Communication + Output + Processing + Input + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + comm_bind + + + + + + + + + + + + + + + + + + weak/comm_link + + + + + + + + + + + + + + + + + + - comm_order +- comm_alias + + + + + + + + + + commop(,,) + + + + + + + + + + weak/scan + + + + + + + + + + + + + + + + + + comm_reports_type + + + + + + + + + + + + + + + + + + comm_reports + + + + + + + + + + + + + + + + + + comm_halt + + + + + + + + + + + + + + + + + + comm_impl + + + + + + + + + + + + + + + + + + callguard(..) + + + + + + + + + + + + + + Propagation + + + + + + + + + 5 + + + + + + + + + + + + + + + dfa_uppy + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/documentation-api/latex.graphml b/documentation-api/latex.graphml index 96adb5a..c537821 100644 --- a/documentation-api/latex.graphml +++ b/documentation-api/latex.graphml @@ -1,819 +1,819 @@ - + Latex Compilation Transcend - Interpretation + Interpretation - + ExtraArgs FnInvocation - + Latex BruteScope Dec - + ICodeScopeUnit - + Latex BruteFunction Dec - + IFunctionUnit - + getSubjectDomain - + Latex Query - + IQuery - + collapseColumn - + Latex Query - + represent Trans Expression Latex script Latex script Latex Output Processing Input Demand upstream latex_scope_demand latex_registered_subjects scope_demand(1) fn_demand decision scope_demand(2) late(decision) scope_fn fn_demand_ordered latex_symbol - + - + - - + + diff --git a/documentation/Concepts/context.xml b/documentation/Concepts/context.xml index 8f9fc49..3762cb8 100644 --- a/documentation/Concepts/context.xml +++ b/documentation/Concepts/context.xml @@ -1,311 +1,365 @@ - Context + - Computer program and its internal states and transitions between them - can be looked at from two different points of view: control flow and data - flow. Any information that can be derived from control flow is called - context in Xreate. + <?xxe-sn 2ahi4rjnvuo 2?>Context - Data that can be captured from analysing control flow consists of two - parts as follows: + Computer program and its internal states and + transitions between them can be looked at from two different points of view: + control flow and data flow. Any information that can be derived from control + flow is called context in + Xreate. + + Data that can be captured from analysing + control flow consists of two parts as follows: + + - Instantaneous state or current place within the code. It's fully - determined by current code block as well as hierarchy of all its - respective parents + + + Instantaneous state or current place + within the code. It's fully determined by current code block as well as + hierarchy of all its respective parents - Historical data determined by all previous visited code - blocks + + + Historical data determined by all previous + visited code blocks - Xreate allows to express Context and reason about it by employing - block level annotations. See syntax. + Xreate allows to express Context and reason + about it by employing block level annotations. See syntax.
- Examples of Context Usage: Suggestions and Requirements + - //someStringFn = function:: string {...} + <?xxe-sn 2ahi4rjnvuo e?>Examples of Context Usage: Suggestions and + Requirements + + //someStringFn = function:: string {...} main = function:: string; entry { context:: env(utf8). someStringFn() } - Example shows annotation env(utf8) which conveys some - information about the block thus distinguishing it from the others. It - allows compiler to apply specific compilation rules for this block. - Suppose someStringFn has different specializations for - different environments. Now it's possible to invoke specialization - tailored for UTF8 environment. + Example shows annotation env(utf8) + which conveys some information about the block thus distinguishing it from + the others. It allows compiler to apply specific compilation rules for + this block. Suppose someStringFn has + different specializations for different environments. Now it's possible to + invoke specialization tailored for UTF8 environment. - Different story with the next example. Here we want to stipulate - context properties: + Different story with the next example. Here + we want to stipulate context properties: - guard:: safe + name - "...." +guard:: safe { crucialOperation = function:: int {0} } main = function:: int; entry { context:: env(safe). crucialOperation() } - Function crucialOperation has only one specialization - safe in the example. If context does not provide required - environment env(safe)compiler can't find appropriate - specialization and halts with compilation error. This is a way for - function to express requirements or contract to a - context it works within. + Function crucialOperation + has only one specialization safe in + the example. If context does not provide required environment + env(safe)compiler can't find + appropriate specialization and halts with compilation error. This is a way + for function to express requirements or contract + to a context it works within.
- Context Propagation + + + <?xxe-sn 2ahi4rjnvuo r?>Context Propagation - Context of a particular code block contains not only its own - annotations but also reflects parent blocks as well as previously executed - blocks. It's achieved by context propagation. + Context of a particular code block contains + not only its own annotations but also reflects parent blocks as well as + previously executed blocks. It's achieved by context + propagation. - Context propagation means that nested blocks - inherit context of parents. Moreover callee - function's context inherits caller's one. Example: + Context propagation means that nested blocks + inherit context of parents. + Moreover callee function's context inherits caller's one. Example: - //requires 'safe' context + name = "..." +//requires 'safe' context guard:: safe { crucialOperation = function(a:: int, b::int):: int { 0 } } test = function:: int; entry { //blockA context:: env(safe). range = [1..10]:: [int]. loop fold(range->x::int, 0->acc):: int { //blockB crucialOperation(x, acc) // In the nested scope env(safe) context still accessible } } - This is example of nested scope context - propagation. It demonstrates availability of a - env(safe) annotation in the context of the nested block - blockB despite being declared in blockA. + This is example of nested + scope context propagation. It demonstrates availability of a + env(safe) annotation in the context + of the nested block blockB despite + being declared in blockA. - More complicated case is inter-function context + More complicated case is + inter-function context propagation. It means context propagates through "caller/callee" relation: callee inherits caller context. The example below demonstrates this: - toSI = function(x:: int):: int + name = "..." +toSI = function(x:: int):: int { 0 } calculate = function(x:: int):: int { y = toSI(x):: int. y } test = function:: int; entry { context:: units(millimeters). calculate(10) } - Suppose calculate()works with values measured in - different units. It normalizes each value by invoking toSI() - conversion. One approach is to keep unit information for each variable - independently. But if we know that entire program or a part of it works - only with specific unit we can register it in a context, - units(millimeters)in this example, and - calculate() and its callees inherit context allowing compiler - to generate code tailored for specific units only. - - Context is determined by reasoning over control flow graph of a - program during compilation. Let's consider example: - - calcInches = function:: int + Suppose calculate()works + with values measured in different units. It normalizes each value by + invoking toSI() conversion. One + approach is to keep unit information for each variable independently. But + if we know that entire program or a part of it works only with specific + unit we can register it in a context, units(millimeters)in + this example, and calculate() and + its callees inherit context allowing compiler to generate code tailored + for specific units only. + + Context is determined by reasoning over + control flow graph of a program during compilation. Let's consider + example: + + name = "..." +calcInches = function:: int { context:: precision(accurate); units(inches). calculate() } calcMillis = function:: int { context:: precision(accurate); units(millimeters). calculate() } calculate = function:: int { 0 } - Client functions calcInches() and - calcMillis() each define context with a configuration options - for a main routine calculate(). Unlike in previous example, - there are several callers with different context here. - - In case with several possible control flow paths each introducing - different context, only path invariant context annotations could be - determined at compile time. Obviously, annotations that are the same for - each possible alternative are part of context in any case. It's - precision(accurate) in the example above, since both client - function define it. More formally, statically determined context is a - conjunction of all possible contexts of a given code block. - - However the other annotation units(...) differs from - path to path and can be determined only during runtime. Late Transcend - functionality is used for this. Context reasoning employing Late Transcend - called Late Context or Latex for - short. + Client functions calcInches() + and calcMillis() each define context + with a configuration options for a main routine calculate(). + Unlike in previous example, there are several callers with different + context here. + + In case with several possible control flow + paths each introducing different context, only path invariant context + annotations could be determined at compile time. Obviously, annotations + that are the same for each possible alternative are part of context in any + case. It's precision(accurate) in + the example above, since both client function define it. More formally, + statically determined context is a conjunction of all possible contexts of + a given code block. + + However the other annotation + units(...) differs from path to path + and can be determined only during runtime. Late Transcend functionality is + used for this. Context reasoning employing Late Transcend called + Late Context or + Latex for short.
- Latex (Late Context) + + + <?xxe-sn 2ahi4rjnvuo 1n?>Latex (Late Context) - Static(compile-time) context reasoning is weak - since it's able to infer only partial context, consisting of properties - that are true for all possible paths leading in a CFG to a given block. - Other part consists of set of possible properties that depends on exact - path in CFG. Such uncertainty possible to resolve during runtime once it's - known which path is chosen. + Static(compile-time) context reasoning is + weak since it's able to + infer only partial context, consisting of properties that are true for all + possible paths leading in a CFG to a given block. Other part consists of + set of possible properties that depends on exact path in CFG. Such + uncertainty possible to resolve during runtime once it's known which path + is chosen. - It leads to a necessity of having //late context// - context data - gathered on relevant occasion at runtime to determine right - decisions. + It leads to a necessity of having //late + context// - context data gathered on relevant occasion at runtime to + determine right decisions. - However, for any cases it's crucial to consider //possible - contexts// that is, contexts valid only under certain conditions. + However, for any cases it's crucial to + consider //possible contexts// that is, contexts valid only under certain + conditions. - Latex approach can be described as follows: + Latex approach can be described as + follows: + + - All possible alternative contexts for the given scope computed - during compile time used as input for Latex + + + All possible alternative contexts for + the given scope computed during compile time used as input for + Latex - All possible paths are numerated and specific latex parameter - created to keep data about current path. + + + All possible paths are numerated and + specific latex parameter created to keep data about current + path. - Late parameter used as guard for Late Transcend facts context - consists of. + + + Late parameter used as guard for Late + Transcend facts context consists of. - As of now, to convey late context data latex parameter injected into - function signature as hidden parameter. + As of now, to convey late context data + latex parameter injected into function signature as hidden + parameter. - import raw ("core/control-context.lp"). + name = "..." +import raw ("core/control-context.lp"). compute = function:: int { 0 } computeFast = function:: int { context:: computation(fast). compute() } computePrecisely = function:: int { context:: computation(precise). compute() } test = function(cmnd:: int):: int; entry { context:: arithmetic(iee754). if (cmnd > 0)::int {computePrecisely()} else {computeFast()} } - Static scope + Static scope - + - import raw ("core/control-context.lp") + name = "..." +import raw ("core/control-context.lp") case context:: computation(fast) { compute = function:: num { 0 } } case context:: computation(precise) { compute = function:: num { 0 } } executeComputation= function:: num { compute() } test = function(cmnd:: num):: num; entry { if (cmnd > 0)::num { context:: computation(fast). executeComputation() } else { context:: computation(precise). executeComputation() } } - To sum up, context consists of two complements parts: on the one - hand //static(early) context// denotes compile time inferences, + To sum up, context consists of two + complements parts: on the one hand //static(early) context// denotes + compile time inferences, - and on the other hand, //late(dynamic) context// denotes annotations - decided upon at runtime. + and on the other hand, //late(dynamic) + context// denotes annotations decided upon at runtime. - Since it is possible to determine number of possible contexts with - diffent outcome decisions, it is possible to determine least size for - late context data enough to identify each possible variant. (In example - above, since there are only two specializons of `compute`, 1 bit is - enough to convey late context data) + + + Since it is possible to determine number + of possible contexts with diffent outcome decisions, it is possible to + determine least size for late context data enough to identify each + possible variant. (In example above, since there are only two + specializons of `compute`, 1 bit is enough to convey late context + data)
- Remarks on late context implementation + + + <?xxe-sn 2ahi4rjnvuo 2a?>Remarks on late context + implementation - + - To return to a last example, in order to correcly determine - `compute`'s context it's necessary: + To return to a last example, in order to + correcly determine `compute`'s context it's necessary: - After such transformation signature of `executeComputation` looks - like `executeComputation(__hidden_context_data__)`, + After such transformation signature of + `executeComputation` looks like + `executeComputation(__hidden_context_data__)`, - where `hidden_context_data` holds data enough to determine within - `executeComputation` which one of possible contexts it encountered - with. + where `hidden_context_data` holds data + enough to determine within `executeComputation` which one of possible + contexts it encountered with. - Consequently, `executeComputation` decides which specialization of - `compute` should be called based on `hidden_context_data` value. + Consequently, `executeComputation` decides + which specialization of `compute` should be called based on + `hidden_context_data` value. - Only at run-time there is enough information for - `executeComputation` to decide what specialization of `compute` to - call. + Only at run-time there is enough + information for `executeComputation` to decide what specialization of + `compute` to call.
diff --git a/documentation/communication.xml b/documentation/communication.xml new file mode 100644 index 0000000..8c945f9 --- /dev/null +++ b/documentation/communication.xml @@ -0,0 +1,440 @@ + + + + + <?xxe-sn 29tvny21340 2?>Communication + + 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. + +
+ + + <?xxe-sn 29xq7jt0wzk 2?>Syntax + + Annotations: + + SYNTAX: +**commop(send)** (1) +**commop(receive)** (2) + + + + + + + + annotation (1) + marks SEND communication + event. + + + + + + annotation (2) + marks RECEIVE communication + event. + + + + Specializations: + + SYNTAX: +**commDirect** +**commGuarded** + + Communication reasoning able to assign + following specializations: + + + + + + + + commDirect + — specialization is expected to provide direct access to raw + variable's content. + + + + + + commGaurded + — specialization is expected to do internal consistency checks at run + time. + + +
+ +
+ + + <?xxe-sn 29tvny21340 4?>Background + + One of the major concepts that support + writing of safe programs is a notion of immutability. + 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 communication + model is discussed next. +
+ +
+ + + <?xxe-sn 29xq7jt0wzk 6?>Communication Model + + Communication + model 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 sending, + and conversely reading variable's value is viewed as receiving. + + 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 communication + model due to similarity with the network communication. + + Reasoning based on working with a + communication path, i.e chain + of communication events(e.g. + sending/receiving) occurred during program execution. + + Let's consider small example: + + a = init():: int; comm(send). //(1) +b = a + 1 :: int; comm(receive). //(2) + + It shows computing of variable + b. Variable b + depends on a so a + is calculated first. Variables a, + b are annotated with comm(send) + and comm(receive), denoting + sending and + receiving events, + respectively. Communication path in this case is an ordered list + {<begin>, SEND, RECEIVE, + <end>} where <begin>, + <end> — are special events that denote first and last events + in the path, respectively. + + The gist of using communication model is to + ensure that every sent value is properly + received. 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: + + + + + + + + Validation. In this mode all + communication paths are checked against communication rules to confirm + that the program is valid. Otherwise compilation error is + raised. + + + + + + Planning. In this mode reasoning assigns + proper implementation for variables in efforts to ensure + validity. + + +
+ +
+ + + <?xxe-sn 29xq7jt0wzk k?>Validation + + 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: + + + + + + + + Valid. Path that consists of pairs of + events {SEND, RECEIVE} are + valid meaning that each + sent value is properly received. + + + + + + Undefined and expired value. Paths that + have parts {<begin>, + RECEIVE} or {RECEIVE, + RECEIVE} 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. + + + + + + Lost value. Paths that have parts + {SEND, SEND} or {SEND, + <end>} 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. + + + + 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 value + expiration after it was used as well as value + loss, if it was not used at + all. +
+ +
+ + + <?xxe-sn 29xq7jt0wzk 2a?>Planning + + 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: + + + + + + + + Direct. Direct specialization + commDirect is expected to provide + direct access to variable's value. This specialization is assigned in + case of fully statically validated communication path. + + + + + + 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 commGaurded + is expected to hold variable state and check usage consistency. + + +
+ +
+ + + <?xxe-sn 2a3uy8rr2f4 9?>Planning Horizon + + Reasoning implements algorithm that is + bounded by the maximal path length it can process. The parameter is called + planning horizon. Any + variable that it can not check due to exceedingly large path's length is + assigned default implementation commGaurded + that performs necessary checks during runtime. Thus the parameter + regulates trade off between static analysis extensiveness and runtime + checks overhead. +
+ +
+ + + <?xxe-sn 2a7t1hxqqyo 2?>Example: Direct Implementation + + 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 +} + + In this example, basic workflow is presented + in main — the function + write(x1, 1) is invoked following by + invocation of read(x2). Functions + write() and read() + are annotated with commop(send) and + commop(receive) 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 CommDirect + 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. +
+ +
+ + + <?xxe-sn 2a7t1hxqqyo a?>Example: Guarded Implementation + + 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 +} + + Here example of slightly more complicated + workflow. Function main 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 + SEND events. In this situation the + analyzer unable to statically validate correctness and assigns + specialization commGuarded to embed + checking logic into compiled code as an intermediary layer between + variable's content and client's code. Implementation commGuarded + along with a variable access also tracks the variable status and returns + error if the value is inconsistent. +
+ diff --git a/documentation/exploitation.xml b/documentation/exploitation.xml index 43ac71c..984d077 100644 --- a/documentation/exploitation.xml +++ b/documentation/exploitation.xml @@ -1,487 +1,488 @@ <?xxe-sn 26yv439af40 2?>Exploitation This chapter discusses exploiting external resources, such as files, as a particular instance of a side effects problem that inevitably stems from an interaction with the outside world. Unlike virtualization, an another documentation's topic that tackles I/O, exploitation approaches subject from a different angle — it is concerned with an order of operations, sequence in which different clients jointly use the same resource and it deals with corresponding difficulties, e.g. ensures proper resource initialization before actual usage.
<?xxe-sn 29je46abuev -wunr7fl0rw8u?>Syntax
<?xxe-sn 29je46abuev -wunr7fl0rw8r?>Annotations SYNTAX: **use**(//resource-id//) **init**(//resource-id//) resource-id — user-defined resource identifier Annotates function or code - block as such that exploits resource resource-id. - + block as such that exploits resource resource-id.
<?xxe-sn 29je46abuev -wunr7fl0rw8i?>Guards SYNTAX: **exploitation(init)** **exploitation(none)** Specializations that are recognized by exploitation reasoning. Each specialization corresponds to an initialization strategy: exploitation(init) is expected to perform actual resource initialization. exploitation(none) is expected to do nothing as initialization isn't necessary or done - elsewhere. + elsewhere.
<?xxe-sn 26yv439af40 4?>Background In software engineering, the idea to avoid side effects have received considerable traction. Indeed, side effects is something that is hard to take into account and thus programs that have side effects are inherently unsafe, thus best coding practices are rightfully suggest to isolate side effects producing code as much as possible. It's so called pure functional languages whose philosophy goes even further and frames side effects as something opposite of "pure", and everything is built around effectless computations to the point that some languages' design itself includes side effects producing constructs, such as I/O, as an afterthought, as something almost unnecessary. However, in reality the opposite is true, most applications' sole responsibility is to communicate with "outside world", reacting to the external events and change "world state" accordingly. As a consequence, side effects usually are the only important effects the program produce and surely deserve first class support from a programming language and justify efforts to develop approach to alleviate related safety and performance concerns.
<?xxe-sn 26yv439af40 10?>Exploitation Plan One complexity of taking side effects into account is the fact that final result depends on an exact operations order. This harshly impacts both performance and safety, for many techniques, e.g. caching, parallelization can neither be automatically performed nor validated since they are based on various degrees of reordering or deal with possibly undetermined beforehand order of execution. In this chapter, it is assumed, that final effects of execution fully defined by exploitation path — for a particular code path that can occur during execution, it is its part consisting of only relevant code blocks., i.e. those that deal with an exploited resource. Other code blocks do not influence exploitation effects and so are excluded from consideration. Thus reasoning about effects is reduced to considering all possible exploitation paths, checking do they meet certain requirements that define valid exploitation and making corrections if needed and possible. Result of the reasoning is called exploitation plan — specification that defines exact order and strategy of using a given resource in order to comply with imposed requirements. With all above said, the discussed approach can be presented as follows: Annotations are used to express some aspects of side effects to enable further reasoning. They indicate code blocks that deal with resource as well as provide additional information about how exactly it is exploited, e.g. use, initialize or deinitialize resource. Existing code paths, extracted during source code processing, coupled with relevant annotations is enough to construct all possible exploitation paths and analyze them. Analysis determines possible(weak) paths that can occur or not during particular execution as well as certain paths(strong) that occur always no matter what. Also it checks are exploitation paths valid against certain rules, e.g. initialization occurs always before actual usage and is it possible to correct invalid paths. Reasoning's result is an exploitation plan that dictates order and strategy of exploitation is presented in form of appropriate specialization for polymorphic functions that deal with resources in order to ensure safe exploitation to the extent based on provided annotations. Exploitation related side effects are viewed as a set of additional restrictions over operations order. Only subset of possible reorders is still valid w.r.t. side effects. Transcend's task is to find out refined set of valid orders. Thus techniques that rely on reordering enjoy additional information to make safe optimizations. ... and it serves three major goals: Safety. Validates existing exploitation plan or is it possible to safely exploit given resource at all. Compiler signals error if a given exploitation plan is invalid, i.e. does not satisfy requirements w.r.t. side effects as expressed by annotations. Regression Resilience. When it comes to using external resources, some spurious dependencies usually occur between otherwise isolated, independent components of a program. Sometimes refactoring and other code changes break those dependencies inevitably introducing regressions. Exploitation catches this sort of regressions and automatically regenerates exploitation plan suited for a changed conditions. Performance. Generated exploitation plans are optimal in a sense that they cut off superfluous operations, for example, removing resource initialization in several places if it can be done safely in a single one, thus reducing overall overhead.
<?xxe-sn 27ay8x1a5mo 2?>Domination Analysis When it comes to a reasoning about order of execution flow and possible code paths, crucial vehicle for that is domination analysis producing dominator tree as an output. Unlike the usual function-bounded domination analysis, when separate domination tree is produced for each function defined in a program, Exploitation requires program bound analysis, that is to take into account control flow across all functions in a program. It is computationally intensive task to perform analysis over a whole program, however it is compensated by the fact that Exploitation only takes into account code blocks that deal with, or in other words, exploit external resources. Thus there is no necessity to build full dominator tree, only the relevant parts are constructed, just enough to make sound exploitation plan decisions.
<?xxe-sn 28h47d43thc j?>Empty Exploitation Plan. Effect Free Computations Validation of exploitation path is done against some predefined constraints. Depending on complexity of a constraints, i.e. number of different exploitation events that are seeking for in each path, reasoning goals categorized into several groups: Zero Order Exploitation. Meaning that all paths are checked in terms is there exploitation at all or no, is there at least a single exploitation event along the path. First Order Exploitation. Deals with a situations when it's enough to check only two different exploitation event occur in a required order. It can be useful for example, to check whether all resource uses occur after it is initialized. Higher Order Exploitation. Expresses constraints involving several(more than two) exploitation events and relations between them. Empty Exploitation is an important instance of zero order constraint. It useful mechanism for developer to annotate function or part of a program as effect free in terms of exploitation. Thus, efectless, clean or pure code can be clearly separated from effectfull part and compiler raises compilation error in case of accidental mixing or using "wrong" type of code in non appropriate environment.
<?xxe-sn 26yv439af40 v?>Resource Initialization One important problem related to an exploitation order is to ensure that a given resource is properly initialized before its first usage and additionally it is not initialized more then once during exploitation session. This is instance of first order exploitation since in a validation mode it is enough to check exploitation plan to ensure that every resource usage preceded by resource initialization at some point in the past, i.e. previously in the exploitation path. For planning mode, the problem is addressed as follows: Central idea of the algorithm is to consider candidates for initialization only among code blocks that dominate given usage site. Obviously, initialization in dominating block precedes usage for any possible code path. One or more dominator blocks are chosen for actual initialization in such way that they are cover all found usage sites. For code blocks chosen for initialization specialization exploitation(init) is set, for the rest specialization exploitation(none) is used. Look at the example below: name="tests/exploitation.cpp: Doc_ResourceInit_1", lines=15 import raw("scripts/cfa/payload.lp"). import raw("scripts/exploitation/exploitation.lp"). //exploitation reasoning import raw("scripts/exploitation/test1.assembly.lp"). guard:: exploitation(init) { openFile = function(filePrev:: FILE_P):: FILE_P; init(file) { fopen("/tmp/test", "w")::FILE_P } } guard:: exploitation(none) { openFile = function(filePrev:: FILE_P):: FILE_P { filePrev::int } } test = function:: int; entry { seq { f0 = undef:: FILE_P. f0 } { //Scope #1: f1 = openFile(f0):: FILE_P. f1 } { //Scope #2: f2 = openFile(f1):: FILE_P. f2 } { //Scope #3: sizeWritten = fwrite("Attempt to write..", 12, 1, f2):: int; use(file). sizeWritten } { //Scope #4: fclose(f2):: int; use(file) } { sizeWritten :: int} } There is the function test that executes sequentially next commands: open a file(scopes #1, #2), write some text(scope #3) and finally, close the file(scope #4). It represents simple work flow with an external resource. In order to connect the code to the exploitation the functions fwrite and fclose in scopes #3 and #4 respectively are annotated with annotation use(file). This information is used by reasoning to look whether it is possible to initialize given resource before actual usage as well as where and when exactly to initialize it. Function openFile is annotated as init(file) meaning it can initialize depending on chosen strategy. The function is invoked both in scope #1 and scope #2. Both scopes are executed strictly before scopes #3, #4. Thus it is indeed possible to initialize resource before usage. Next task for exploitation is to choose correct exploitation plan, i.e. to assign strategies for all possible initialization places in the effort to initialize resource only once. Here, it means that only one invocation of openFile is assigned with exploitation(init) to actually initialize the file. Other one is automatically marked with exploitation(none) to invoke different specialization of openFile that does nothing since the files is already initialized.
\ No newline at end of file diff --git a/pandoctl b/pandoctl new file mode 100755 index 0000000..61a06bf --- /dev/null +++ b/pandoctl @@ -0,0 +1,13 @@ +#!/bin/bash + +case $1 in + convert) + Name=$(basename $2) + sed -e '// d' -e 's///g' $2 | \ + /opt/pandoc/dist/build/pandoc/pandoc \ + -f docbook \ + -t ./documentation-tools/doc-converter/remarkup.lua \ + -o /tmp/docs/$Name.remarkup + ;; + *) echo "usage: $0 convert ";; +esac diff --git a/potasscoctl b/potasscoctl new file mode 100755 index 0000000..366a9e3 --- /dev/null +++ b/potasscoctl @@ -0,0 +1,39 @@ +#!/bin/bash + +SOLVER=/opt/potassco/clingo/build/debug/clingo +PLOTTER=/opt/dottoxml/src/dottoxml.py +DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" && pwd )" + +solve () { + #1 - input file + OUTPUT=`$SOLVER -n0 $1` + echo $OUTPUT | sed 's/.*Answer: 1 \(.*\) SATISFIABLE.*/\1/;s/\ /\n/g' +} + +graph () { +# 1 - predicate +# 2 - path +# 3 - filename +# 4 - body + FILE_DOT=$2/$3.dot + FILE_YED=$2/$3.graphml + echo 'digraph xxx {' > $FILE_DOT + echo "$4" | sed -n /^$1\(/p | sed -E "s/$1\((.*),(.*)\)/\1 -> \2\;/g" >> $FILE_DOT + echo '}' >> $FILE_DOT + python $PLOTTER $FILE_DOT $FILE_YED +} +case $1 in + solve) + solve $2 + ;; + graph) + SOLUTION=`solve $3` + OUTPUT_PATH=$(dirname $3) + OUTPUT_NAME=$(basename $3) + graph $2 $OUTPUT_PATH $OUTPUT_NAME "$SOLUTION" + ;; + *) + echo "usage: $0 solve " + echo "usage: $0 graph " + ;; +esac diff --git a/scripts/effects-communication/communication.lp b/scripts/effects-communication/communication.lp index ec62f55..3294291 100644 --- a/scripts/effects-communication/communication.lp +++ b/scripts/effects-communication/communication.lp @@ -1,121 +1,120 @@ %INPUT: % const horizon - Max Depth of communication analysis % comm_order(Alias)), bind(X, comm_alias(Alias) - to apply additional order constraints % dfa_uppy from dfa-propagation % INIT %=========================================================== comm_bind(end, end). comm_bind(begin, begin). comm_bind(X, Op):- bind(X, commop(Op)). % ORDER %============================================================ -comm_path(X2, X1) :- bind(X2, comm_order(Alias)); bind(X1, comm_alias(Alias)). +comm_link(X2, X1) :- bind(X2, comm_order(Alias)); bind(X1, comm_alias(Alias)). % INHERITS %============================================================ -comm_path(X, Y) :- dfa_uppy(X, Y). +comm_link(X, Y) :- dfa_uppy(X, Y). -comm_path(end, X) :- v(X); #sum{1: weak(comm_path(Smth, X)), v(Smth)}0. -comm_path(X, begin):- v(X); #sum{1: weak(comm_path(X, Smth)), v(Smth)}0. +comm_link(end, X) :- v(X); #sum{1: weak(comm_link(Smth, X)), v(Smth)}0. +comm_link(X, begin):- v(X); #sum{1: weak(comm_link(X, Smth)), v(Smth)}0. % SCAN %============================================================ %SOURCE -scan(X, source(X), length(0)) :- comm_bind(X, write). +comm_scan(X, source(X), length(0)) :- comm_bind(X, send). -scan(Z, source(X), length(Length + 1)) :- - comm_path(Z, Y); - scan(Y, source(X), length(Length)); Length < horizon; +comm_scan(Z, source(X), length(Length + 1)) :- + comm_link(Z, Y); + comm_scan(Y, source(X), length(Length)); Length < horizon; not comm_bind(Z, _). -scan(Z, source(X), report(Op)) :- - comm_path(Z, Y); - scan(Y, source(X), length(Length)); Length < horizon; +comm_scan(Z, source(X), report(Op)) :- + comm_link(Z, Y); + comm_scan(Y, source(X), length(Length)); Length < horizon; comm_bind(Z, Op). %SINK -scan(X, sink(X), length(0)) :- comm_bind(X, read). +comm_scan(X, sink(X), length(0)) :- comm_bind(X, receive). -scan(Z, sink(X), length(Length + 1)) :- - comm_path(Y, Z); - scan(Y, sink(X), length(Length)); Length < horizon; +comm_scan(Z, sink(X), length(Length + 1)) :- + comm_link(Y, Z); + comm_scan(Y, sink(X), length(Length)); Length < horizon; not comm_bind(Z, _). -scan(Z, sink(X), report(Op)) :- - comm_path(Y, Z); - scan(Y, sink(X), length(Length)); Length < horizon; +comm_scan(Z, sink(X), report(Op)) :- + comm_link(Y, Z); + comm_scan(Y, sink(X), length(Length)); Length < horizon; comm_bind(Z, Op). % REPORTS %============================================================== comm_reports_type(rprtLostEnd; rprtLost; rprtCorruptNull; rprtDup; rprtOutOfReach). -comm_reports(rprtLostEnd , Source, undef) :- scan(_, source(Source), report(end)). -comm_reports(rprtLost , Source, Spot) :- scan(Spot, source(Source), report(write)). -comm_reports(rprtCorruptNull, Sink, undef) :- scan(_, sink(Sink), report(begin)). -comm_reports(rprtDup , Sink, Spot) :- scan(Spot, sink(Sink), report(read)). +comm_reports(rprtLostEnd , Source, undef) :- comm_scan(_, source(Source), report(end)). +comm_reports(rprtLost , Source, Spot) :- comm_scan(Spot, source(Source), report(send)). +comm_reports(rprtCorruptNull, Sink, undef) :- comm_scan(_, sink(Sink), report(begin)). +comm_reports(rprtDup , Sink, Spot) :- comm_scan(Spot, sink(Sink), report(receive)). comm_halt(Source):- comm_reports(rprtLostEnd, Source, undef). comm_halt(Source):- comm_reports(rprtLost, Source, _). comm_halt(Sink):- comm_reports(rprtCorruptNull, Sink, undef). comm_halt(Sink):- comm_reports(rprtDup, Sink, Spot). % WEAK REPORTS %============================================================= -weak(comm_reports(rprtLostEnd , Source)) :- weak(scan(_, source(Source), report(end))). -weak(comm_reports(rprtLost , Source, Spot)) :- weak(scan(Spot, source(Source), report(write))). -weak(comm_reports(rprtCorruptNull, Sink)) :- weak(scan(_, sink(Sink), report(begin))). -weak(comm_reports(rprtDup, Sink, Spot)) :- weak(scan(Spot, sink(Sink), report(read))). +weak(comm_reports(rprtLostEnd , Source)) :- weak(comm_scan(_, source(Source), report(end))). +weak(comm_reports(rprtLost , Source, Spot)) :- weak(comm_scan(Spot, source(Source), report(send))). +weak(comm_reports(rprtCorruptNull, Sink)) :- weak(comm_scan(_, sink(Sink), report(begin))). +weak(comm_reports(rprtDup, Sink, Spot)) :- weak(comm_scan(Spot, sink(Sink), report(receive))). -comm_reports(rprtOutOfReach, X, Spot) :- weak(scan(Spot, source(X), length(horizon))). -comm_reports(rprtOutOfReach, X, Spot) :- weak(scan(Spot, sink(X), length(horizon))). +comm_reports(rprtOutOfReach, X, Spot) :- weak(comm_scan(Spot, source(X), length(horizon))). +comm_reports(rprtOutOfReach, X, Spot) :- weak(comm_scan(Spot, sink(X), length(horizon))). % SOLUTIONS %============================================================= -comm_impl(Source, commGuarded):- comm_bind(Source, write); +comm_impl(Source, commGuarded):- comm_bind(Source, send); not comm_halt(Source); 1{ weak(comm_reports(Type, Source, _)): comm_reports_type(Type) }. -comm_impl(Source, commDirect):- comm_bind(Source, write); +comm_impl(Source, commDirect):- comm_bind(Source, send); not comm_halt(Source); not comm_impl(Source, commGuarded). bind(Source, callguard(commDirect)):- comm_impl(Source, commDirect). bind(Source, callguard(commGuarded)):- comm_impl(Source, commGuarded). % WEAK ANALYSIS %============================================================= -weak(comm_path(X, Y)) :- weak(dfa_uppy(X, Y)). -weak(scan(Arg1, Arg2, Arg3)) :- scan(Arg1, Arg2, Arg3). +weak(comm_link(X, Y)) :- weak(dfa_uppy(X, Y)). +weak(comm_scan(Arg1, Arg2, Arg3)) :- comm_scan(Arg1, Arg2, Arg3). -weak(scan(Z, sink(X), length(Length + 1))):- - weak(comm_path(Y, Z)); - weak(scan(Y, sink(X), length(Length))); Length < horizon; +weak(comm_scan(Z, sink(X), length(Length + 1))):- + weak(comm_link(Y, Z)); + weak(comm_scan(Y, sink(X), length(Length))); Length < horizon; not comm_bind(Z, _). -weak(scan(Z, sink(X), report(Op))):- - weak(comm_path(Y, Z)); - weak(scan(Y, sink(X), length(Length))); Length < horizon; +weak(comm_scan(Z, sink(X), report(Op))):- + weak(comm_link(Y, Z)); + weak(comm_scan(Y, sink(X), length(Length))); Length < horizon; comm_bind(Z, Op). - -weak(scan(Z, source(X), length(Length + 1))) :- - weak(comm_path(Z, Y)); - weak(scan(Y, source(X), length(Length))); Length < horizon; +weak(comm_scan(Z, source(X), length(Length + 1))) :- + weak(comm_link(Z, Y)); + weak(comm_scan(Y, source(X), length(Length))); Length < horizon; not comm_bind(Z, _). -weak(scan(Z, source(X), report(Op))) :- - weak(comm_path(Z, Y)); - weak(scan(Y, source(X), length(Length))); Length < horizon; +weak(comm_scan(Z, source(X), report(Op))) :- + weak(comm_link(Z, Y)); + weak(comm_scan(Y, source(X), length(Length))); Length < horizon; comm_bind(Z, Op). diff --git a/scripts/effects-communication/example1-wr.xreate b/scripts/effects-communication/example1-wr.xreate index 6d6dc0c..e1f9401 100644 --- a/scripts/effects-communication/example1-wr.xreate +++ b/scripts/effects-communication/example1-wr.xreate @@ -1,41 +1,36 @@ //Only Direct implementatino defined 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"). CommGuard = type variant{Invalid, Valid, Outdated}. CommDirect = type { - value:: int -}. - -CommGuarded = type { - value:: int, - state:: CommGuard + value:: int }. guard:: commDirect { - init=function::CommDirect - { - {value = 0} - } - - read= function(vault1:: CommDirect):: int - { - (vault1:: *;commop(read))["value"] - } - - write= function(vault2:: CommDirect, valueNew:: int)::CommDirect - { - (vault2:: *; dfa_pseudo(vault2)) + {value = valueNew}:: int; commop(write); dfa_uppy(vault2) - } + 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). - a = read(x2)::int; dfa_polym(arg). - a + x1 = init()::*; dfa_polym(ret). + x2 = write(x1, 1)::*; dfa_polym(arg). + a = read(x2)::int; dfa_polym(arg). + a } diff --git a/scripts/effects-communication/example2-wr.xreate b/scripts/effects-communication/example2-wr.xreate index 7a53acd..1d59688 100644 --- a/scripts/effects-communication/example2-wr.xreate +++ b/scripts/effects-communication/example2-wr.xreate @@ -1,76 +1,76 @@ //Direct and Guarded implementation defined 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"). CommGuard = type variant{Invalid, Valid, Outdated}. CommDirect = type { value:: int }. CommGuarded = type { value:: int, state:: CommGuard }. guard:: commDirect { init=function::CommDirect{ {value = 0} } read= function(vault1:: CommDirect):: int{ - (vault1::CommDirect; commop(read))["value"] + (vault1::CommDirect; commop(receive))["value"] } write= function(vault2:: CommDirect, valueNew:: int)::CommDirect{ - (vault2::CommDirect;dfa_pseudo(vault2)) + {value = valueNew}:: int; commop(write); dfa_uppy(vault2) + (vault2::CommDirect;dfa_pseudo(vault2)) + {value = valueNew}:: 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::CommGuarded;commop(read)):: int + switch variant (vault3::CommGuarded;commop(receive)):: int case (Invalid) { errorRead() } case (Outdated) { errorRead() } case (Valid) { vault3["value"] } } write=function(vault4:: CommGuarded, valueNew:: int)::CommGuarded{ switch variant (vault4)::int case (Invalid) { {value = valueNew, state = Valid()} } case (Outdated) { {value = valueNew, state = Valid()} } case (Valid) { errorWrite() } } } main=function::int; entry { x1 = init():: *; dfa_polym(ret). x2 = write(x1, 1)::*; dfa_polym(arg). a = read(x2):: int; dfa_polym(arg). a } diff --git a/scripts/effects-communication/example3-wrwr.xreate b/scripts/effects-communication/example3-wrwr.xreate index 39f6f89..773ae0e 100644 --- a/scripts/effects-communication/example3-wrwr.xreate +++ b/scripts/effects-communication/example3-wrwr.xreate @@ -1,86 +1,84 @@ -//Direct and Guarded implementation defined - 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"). -CommGuard = type variant{Invalid, Valid, Outdated}. +CommState = type variant{Invalid, Valid, Outdated}. CommDirect = type { value:: int }. CommGuarded = type { value:: int, - state:: CommGuard + state:: CommState }. guard:: commDirect { init=function::CommDirect{ {value = 0} } read= function(vault1:: CommDirect):: int{ - (vault1::CommDirect; commop(read))["value"] + (vault1::CommDirect; commop(receive))["value"] } write= function(vault2:: CommDirect, valueNew1:: int)::CommDirect{ - (vault2::CommDirect;dfa_pseudo(vault2)) + {value = valueNew1}:: int; commop(write); dfa_uppy(vault2) + (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::CommGuard;commop(read)):: 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::CommGuard;commop(write); dfa_pseudo(vault4))::int + 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 }