[qvts] Multi-level speculation

[eclipse-qvtd-bot]

| --- | --- | | Bugzilla Link | 515490 | | Status | NEW | | Importance | P3 normal | | Reported | Apr 20, 2017 03:30 EDT | | Modified | Apr 19, 2019 04:30 EDT | | Depends on | 530937 | | See also | 512738, 545245 | | Reporter | Ed Willink |

Description

Bug 512738 identifies that the QVTr

when { if A(...) then B(...) else C(...) endif; }

may require conditional invocation of B/C after A. Note that if A succeeds and then B fails, the 'success' of A must not affect output models.

This presumably undermines the single speculation currently envisaged. A cascade of speculations may be necessary to gradually chip away at the problem.

[eclipse-qvtd-bot]

By Ed Willink on Mar 10, 2019 07:07

Consider a partial Dining Philosophers problem.\ Init: philosopher.hasLeft=?, philosopher.hasRight=?, philosopher.hasEaten=?, fork.holder=?\ Rule 1. Pick up Left Fork. => philosopher.hasLeft = true, leftFork.holder = philosopher;\ Rule 2. Pick up Right Fork. => philosopher.hasRight = true, rightFork.holder = philosopher;\ Rule 3. Eat provided hasLeft=true, philosopher.hasRight=true => philosopher.hasEaten = true.

A fuller solution requires multiple assignment and consequently multiple distinct in-place 'rounds', which may justify passing the buck to the programmer to provide a valid 'schedule'. The minimal example can reasonably be regarded as a single composite execution, with Rule 3 being a typical second pass after an R1/R2 first pass. This is one for which the magic of Declarative execution is responsible for the schedule.

Depending on scheduling order, some philosophers may get some forks and eat.

A rule-based execution might do Rule 1 to exhaustion and go straight to 'deadlock'. => N successes of R1

A pass-based execution might do a mix Rule 1's and Rule 2's => ??

An object-based execution might fully feed half the philosphers. => N/2 successes of R1, N/2 successes of R2, N/2 successes of R3

What is the 'correct' execution? It it an illegal transformation? Is 3N/2 better than N, if so which phiosophers eat? Can speculation find a 'correct' solution? Does a general speculation need to examine an NP-complete search space?

[eclipse-qvtd-bot]

By Ed Willink on Mar 10, 2019 07:09

R1 and R2 have no guard. We therefore have an assignment conflict between "leftFork.holder = philosopher" and "rightFork.holder = philosopher". This is a statically detectable hazard, but could be ok for some data configurations.

If R1 and/or R2 had an explicit guard, the tested value would be two-valued. R1 and R2 have the implicit guard that philosopher.hasLeft and leftFork.holder is unassigned.

---

If we implement and run, it fully feeds 3 out of 3 philosophers. Oops. It seems that a multi-assignment to the fork status is ignored.

[eclipse-qvtd-bot]

By Ed Willink on Apr 18, 2019 05:45

The poor style of the QVTc SimpleUML2RDBMS really needs a multi-stage local predicate. See comment in LocalPredicatePartitionFactory.gatherReachableOldAcyclicNodes

[eclipse-qvtd-bot]

By Ed Willink on Apr 19, 2019 04:30

non-top when invocations (as in ATL2QVTR whe mapVariable) require multi-stage.

a) realize the 'shared' trace with a realized edge to its input, predicated edge to its output/success.

b) the subsequent real predication.

Currently implemented as an extra <> partition.