Community
Participate
Working Groups
The Forward2Reverse example has two mutually dependent mappings requiring potentially intractable static analysis to break the chicken-egg loop. It would appear to be necessary to perform speculative creation of trace/output objects to allow creation-dependent guards to evaluate. If these guards fail the speculative creations must be discarded before incorporation in any result / cache. cf ATL does speculative creation but doesn't classify it as such and so fails to discard its consequences.
(In reply to Ed Willink from comment #0) > If these guards fail the speculative creations must be discarded before > incorporation in any result / cache. Partitioning into - speculation partition, creates middle realized object (trace) - speculated partition, creates non-middle realized objects - assignment partitions, creates residual assignments means that only an unwanted middle realized object is created. Nothing in the output models needs discarding. The combination of navigation-to-null predicates, failed speculation provides many of the functionalities of GT's Negative Application Conditions. For very awkward cases, it may be necessary to have a global arbitration between speculation and speculated to determine whether global speculation has a globally consistent solution. Perhaps the realized outputs are distinguished as corrolaries since a successfully speculated trace objects guarantees the creation of the realized outputs. A predicate on a corrolary can be pruned from the residual global predicate satisfaction analysis.
Introduction of speculation and speculated phases has been done as part of Bug 498400. This bug addresses the residual awkward case of speculations whose predicates involve predicated rather than loaded inputs. Fortunately this doesn't seem to be a common requirement.
(In reply to Ed Willink from comment #2) > residual awkward case of speculations whose predicates involve predicated The speculation partition is a valid partial execution creating the middle trace object wrt the loaded/constant inputs. Partial since all predicated predicates are ignored (and no middle-creations or assignments are performed.) Any subsequent use of the middle trace object speculation that continues to ignore the predicated predicates is unsound. (Current code exploits the rarity of this case.) Therefore every use of a speculated middle should also express the missing predicated predicate at the point of use. This leaves everything consistently defined by dependencies so that the scheduler should find a static schedule where possible or dynamic otherwise. --- Alternatively if we try to avoid the repetition of expressing the predicated predicate in every use, we could could have a Boolean state for a speculated middle. false after the loaded-only speculation, true after a further predicated-too speculation. This avoidance costs an additional speculation mapping, requires evaluate-time support for this Boolean state and may have deadlocks if the inter-predicated predicate dependencies are unhelpful requiring a true execution. --- expressing the predicated predicate in every use seems much simpler and their are not that many users of each middle. Rather than avoiding the overhead it may be better to look for a more general global dependency pruning/sharing to optimize this and other bloats. But, is every overall solution guaranteed not to deadlock while speculation discovers it?
(In reply to Ed Willink from comment #0) > potentially intractable static analysis to break the chicken-egg loop. Bug 532429 outlines a compile-time speculation analysis that may often render run-time support redundant.
Bug 540797 identifies deficiencies in the globalSuccess trace property determination.
