Remarks and Questions on the Monotone Framework

AlexanderF
BASIC-Programmierer
BASIC-Programmierer
Beiträge: 140
Registriert: 2. Mai 2010 17:55

Remarks and Questions on the Monotone Framework

Beitrag von AlexanderF » 10. Nov 2017 21:23

hello,

In the Monotone Framework (Module 2, slide 68) we assume a complete lattice
where each subset of L has a least upper bound and a greatest lower bound (slide 52).
In the presented analyses (slides 73ff) we only use finite sets (like the power set of all variables resp. nontrivial subexpressions occurring in the program). Hence I think it suffices to assume that just finite subsets have a least upper bound resp. a greatest lower bound.

We also use only the least upper bound, not the greatest lower bound.
(In the Available Expressions Analysis for example, we use therefore the "dual lattice" (slide 74).)
So I think we do not really need a lattice, but it suffices to assume a (join-)semilattice.

On slide 80 we use three dimensions (powerset lattice/dual powerset lattice, forward/backward and smallest/largest solution) to characterize instances of the Monotone Framework. Does it not depend on the choice of the powerset/dual powerset lattice, whether one looks for the smallest or the largest solution? If we use the powerset lattice (May Analyses, where we take the Union of the neighbor solutions) we are looking for the smallest solution (slide 38) (since the whole set of variables trivially solves the equation). If we use the dual power set lattice (Must Analyses, where we take the Intersection of the neighbor solutions) we are looking for the largest solution (slide 32) (since the empty set trivially solves the equation). So are this actually not three dimensions, but two?

Best Regards,
Alexander

ximl
Erstie
Erstie
Beiträge: 12
Registriert: 4. Okt 2017 17:12

Re: Remarks and Questions on the Monotone Framework

Beitrag von ximl » 1. Dez 2017 14:48

Hi Alexander,

In general, the Monotone Framework enables one to
express analyses over an infinite domain (e.g., the
constant propagation analysis). Correspondingly, the
Monotone Framework comes with the assumption of a
complete lattice, where a least upper bound exists for
all subsets including the infinite ones.

Concerning the need for greatest lower bounds, note
that in a join semi-lattice without the GLB requirement,
a monotone function does not necessarily have a least
fixed point. However, the existence of least fixed points
is so that there is always a most desired solution for the
data flow analysis of concern.

On slide 80, the table is **not** meant to express
independence between characteristics of the four analyses.
So your observation on the dependence between some
of the dimensions is correct.

Best regards,
Ximeng

AlexanderF
BASIC-Programmierer
BASIC-Programmierer
Beiträge: 140
Registriert: 2. Mai 2010 17:55

Re: Remarks and Questions on the Monotone Framework

Beitrag von AlexanderF » 4. Dez 2017 14:28

I think in my first question I should have argued with the finite branching factor instead of the finiteness of the sets.
Also I have seen in the meanwhile that we need the complete lattice in the Tarski’s Fixed Point Theorem to ensure that we have fixpoints and a least fixpoint.
And thank you for the answer.

best regards,
Alexander

Antworten

Zurück zu „Archiv“