search

eclipse-qvtd / org.eclipse.qvtd

Eclipse Public License 2.0
0 stars 0 forks source link

[schedule] Support compile-time speculation #341

Open eclipse-qvtd-bot opened 1 day ago

eclipse-qvtd-bot commented 1 day ago

| --- | --- | | Bugzilla Link | 532429 | | Status | NEW | | Importance | P3 major | | Reported | Mar 14, 2018 04:54 EDT | | Modified | Nov 26, 2018 11:37 EDT | | Blocks | 541527, 498295, 513375, 515236 | | Reporter | Ed Willink |

Description

Introduction of the direct QVTr2QVTs and better support for overriding reveals that the Forward2Reverse example has worked because some success predicates were assumed. Once they are added the example deadlocks in the absence of run-time speculation support from Bug 498295.

For complex data-dependent execution run-time speculation is necessary, but for a perhaps very large class of problems such as Forward2Reverse speculation can be resolved at compile time and the generated mappings simplified accordingly.

Problems amenable to compile-time analysis involve:

It should be possible to setup a type-based dependency graph so that nodes represent all Txxx successful or all X::y assigned and propagate these existential truths. Since the XXX input to TXXX2YYY trace is frequently to-exactly-one, we have may truths with which to send this graph.

MAJOR since the current fudge that speculation always succeeds is sure to lead to some wasted unpleasant debugging experiences.

AND where compile-time speculation is impossible we must have a warning that run-time execution is not implemented yet.

eclipse-qvtd-bot commented 1 day ago

By Ed Willink on May 15, 2018 04:58

ATL2QVTr is quite interesting for this. It performs a uniform mapping on a composition tree. There are many types so there is a polymorphic family of relations. Expressions have child expressions so the relations are cyclic. Naively this needs run-time resolution, however a bottom up creation could be unconditionally successful. We just need to identify that all relations in the cycle succeed.

A new InfallibilityAnalysis supports this analysis. But it doesn't help (yet).

We need to identify that a polymorphic family always succeeds, although obviously all but one should fail. This requires proof that the sum of e.g.

in mapNavigationOrAttributeCallExp_Helper\ atlAttributes : Sequence(atloclMM::Attribute) = atlModule.elements->selectByKind(atlMM::Helper)._definition.feature->selectByKind(atloclMM::Attribute)->select(name=propertyName)\ atlAttributes->notEmpty();\ \ in mapNavigationOrAttributeCallExp_Property\ atlAttributes : Sequence(atloclMM::Attribute) = atlModule.elements->selectByKind(atlMM::Helper)._definition.feature->selectByKind(atloclMM::Attribute)->select(name=propertyName)\ atlAttributes->isEmpty();\ \ is true.

Potentially this may require full logic capability, but the above actually involves just selections whose inverse are easy

Does a logic of selections cover a usefully large section of override discriminations?

eclipse-qvtd-bot commented 1 day ago

By Ed Willink on Nov 23, 2018 11:11

(In reply to Ed Willink from comment #1)

A new InfallibilityAnalysis supports this

Correction: FallibilityAnalysis.

Naively this needs run-time resolution, however a bottom up creation could be unconditionally successful. We just need to identify that all relations in the cycle succeed.

For the most general case success proofs are necessary. But two special cases can be easier.

If removal of all child production edges makes a cycle acyclic, it is top down iteration. Alternatively if removal of all parent production edges makes a cycle acyclic it is bottom up. No need to consider override coverage; just the containment edge. (A child production predicates the container and realizes the contained element. Vice-versa parent production.)

eclipse-qvtd-bot commented 1 day ago

By Ed Willink on Nov 24, 2018 04:09

(In reply to Ed Willink from comment #2)

(A child production predicates the container and realizes the contained element. Vice-versa parent production.)

Not nearly so simple.

The output realized composition edge could be in a late mapping outside the loop.

A tree-to-flat tx has only input composition to work with, whereas a flat-to-tree has only output composition. It seems we need to identify a logical trace-class composition tree. See also Bug 541527.

A trace class/dispatcher provides a lookup index in the forward direction between a compound predicated input node to a compound realized output node, where a compound node is a group of similarly predicated/realized nodes related by non-composition 1-to-1 edges (?? to-1 will do ??). Where there is a composition relationship between nodes in two compound nodes in the same relation, there is a logical trace class composition.

The pathological case of conflicting input/output composition directions implies a daisy-chain to inverse daisy-chain that can be adequately handled by falling-back to the no-composition approach.

Early Analysis Step: analyze the relations to discover logical trace class compositions.

Cycle Step: eliminate trace class compositions to break cycle.

eclipse-qvtd-bot commented 1 day ago

By Ed Willink on Nov 26, 2018 11:37

(In reply to Ed Willink from comment #2)

For the most general case success proofs are necessary. But two special cases can be easier.

If removal of all child production edges makes a cycle acyclic

No. No. No. We do not remove edges from cycles, rather we prove that a cycle halts all by itself.

Detecting infallible mappings proves that a whenXXX.success edge is to-true (and so redundant.) If all mappings in the cycle are infallible, the cycle terminates.

Detecting containment can prove that the cycle terminates. If some mapping fails, the cycle predecessors succeed, but their products will fail to integrate at the failing mapping. If the cycle predecessors were intended to fail, they should have had further when predicates.

Failure to establish termination at compile-time requires run-time speculation to detect a deadlock and fail accordingly.