Orphan Shadow Analysis

Moderator: Automated Software Engineering

LordHoto
BASIC-Programmierer
BASIC-Programmierer
Beiträge: 135
Registriert: 14. Dez 2009 17:00

Orphan Shadow Analysis

Beitrag von LordHoto » 27. Feb 2012 19:01

Hi,

I was wondering about the example for the Orphan Shadow Analysis, it seems the example done on slides 71 till 85, is on source code, which is never shown (at least I can't read the tiny picture in the top right). So I wanted to ask whether someone can please clarify the analysis for me again. As far as I got it so far, as first step one calculates all the "points-to" sets of the varibales. Next one crosses all events, which are used to reach a final state, with the other events in the program. That is in this case the write at w1 and the write at w2, as events required to reach a final state and the close c1 as other event. Now we check whether the variables used in these pairs can point to the same objects, by checking whether the intersection between the points-to sets is not empty. If for one non-critial event, i.e. one which does not be present on the run to a final state, all pairs turn out to have empty intersections, we can safely remove that shadow.

Then again here comes my confusion into this, in the DSM we need a write to reach a final state, thus I don't get why the write at w2 gets deleted. Obviously this could lead to an error state, since we only check for the event to be present and don't do a more sophisticated analysis like in the NopShadow-Analysis.

So if someone please can explain both the OSA and this concrete example to me again, I would be glad, thanks in advance.

// Johannes
Compiler 1 Tutor WS 12/13

Benutzeravatar
ericbodden
Sonntagsinformatiker
Sonntagsinformatiker
Beiträge: 243
Registriert: 5. Apr 2010 19:06

Re: Orphan Shadow Analysis

Beitrag von ericbodden » 28. Feb 2012 09:42

Hi Johannes.
LordHoto hat geschrieben:Hi,
I was wondering about the example for the Orphan Shadow Analysis, it seems the example done on slides 71 till 85, is on source code, which is never shown (at least I can't read the tiny picture in the top right). So I wanted to ask whether someone can please clarify the analysis for me again.
The example abstracts from the source code. We just assume that there are three shadows, as shown on the top right. The actual code is irrelevant to the example.
LordHoto hat geschrieben:As far as I got it so far, as first step one calculates all the "points-to" sets of the varibales. Next one crosses all events, which are used to reach a final state, with the other events in the program. That is in this case the write at w1 and the write at w2, as events required to reach a final state and the close c1 as other event. Now we check whether the variables used in these pairs can point to the same objects, by checking whether the intersection between the points-to sets is not empty. If for one non-critial event, i.e. one which does not be present on the run to a final state, all pairs turn out to have empty intersections, we can safely remove that shadow.
That's true even for critical events. If there are only empty intersections for a shadow "s" then this means that all events raised by this shadow can only point to objects that will never reach the final state (because other crucial events cannot occur on those objects). Hence, the shadow can be dropped.
LordHoto hat geschrieben: Then again here comes my confusion into this, in the DSM we need a write to reach a final state, thus I don't get why the write at w2 gets deleted. Obviously this could lead to an error state, since we only check for the event to be present and don't do a more sophisticated analysis like in the NopShadow-Analysis.
w2 can only refer to objects created at allocation site o2. But there cannot be any close events on those objects - ever: the points-to set of the only close shadow c1 is {o1}. Monitoring "write" on objects that can never be closed is wasted time. Hence w2 can be dropped.

Hope that helps...

Eric
-- Eric

LordHoto
BASIC-Programmierer
BASIC-Programmierer
Beiträge: 135
Registriert: 14. Dez 2009 17:00

Re: Orphan Shadow Analysis

Beitrag von LordHoto » 28. Feb 2012 13:40

ericbodden hat geschrieben:
LordHoto hat geschrieben:As far as I got it so far, as first step one calculates all the "points-to" sets of the varibales. Next one crosses all events, which are used to reach a final state, with the other events in the program. That is in this case the write at w1 and the write at w2, as events required to reach a final state and the close c1 as other event. Now we check whether the variables used in these pairs can point to the same objects, by checking whether the intersection between the points-to sets is not empty. If for one non-critial event, i.e. one which does not be present on the run to a final state, all pairs turn out to have empty intersections, we can safely remove that shadow.
That's true even for critical events. If there are only empty intersections for a shadow "s" then this means that all events raised by this shadow can only point to objects that will never reach the final state (because other crucial events cannot occur on those objects). Hence, the shadow can be dropped.
LordHoto hat geschrieben: Then again here comes my confusion into this, in the DSM we need a write to reach a final state, thus I don't get why the write at w2 gets deleted. Obviously this could lead to an error state, since we only check for the event to be present and don't do a more sophisticated analysis like in the NopShadow-Analysis.
w2 can only refer to objects created at allocation site o2. But there cannot be any close events on those objects - ever: the points-to set of the only close shadow c1 is {o1}. Monitoring "write" on objects that can never be closed is wasted time. Hence w2 can be dropped.
So in the OSA and unlike in the quick check, we check for all the events, which need to be there to reach a final state (in our example automation at least a close + write)? Or do I understand the "for every symbol that is required to reach a final state" wrong, on a first read it sounded to me like this really means just all the symbols which directly enter a final state from *any* other state. But reading your explanation again, it might mean that I need to check every symbol on a path to a final state?

EDIT: To give some example for a DSM with states 1,2,3 (1 being start state, 3 being final state) and events {a,b,c} and a transition relation {(1,a,2) (1,b,2) (2,c,3)} I read that only "c" is a required symbol.
Compiler 1 Tutor WS 12/13

tgp
Sonntagsinformatiker
Sonntagsinformatiker
Beiträge: 268
Registriert: 15. Nov 2006 21:41

Re: Orphan Shadow Analysis

Beitrag von tgp » 28. Feb 2012 13:51

The check "can a final state still be reached?" is already done in the Quick Check analysis:
Paper hat geschrieben:We implement this [quick] check as follows. For each tracematch [automaton representation], we remove edges from its automaton whose label has a shadow count of 0 [= do not appear in the program]. Then we check to see if a final state can still be reached. If the final state can’t be reached, the entire tracematch is removed and all its associated shadows are disabled.

If the quick check fails for a tracematch, i.e. all necessary symbols were applied at least once, we have to change to a more detailed level of abstraction which leads us to the flow-insensitive analysis [OSA].

Benutzeravatar
ericbodden
Sonntagsinformatiker
Sonntagsinformatiker
Beiträge: 243
Registriert: 5. Apr 2010 19:06

Re: Orphan Shadow Analysis

Beitrag von ericbodden » 28. Feb 2012 14:13

LordHoto hat geschrieben:Or do I understand the "for every symbol that is required to reach a final state" wrong, on a first read it sounded to me like this really means just all the symbols which directly enter a final state from *any* other state. But reading your explanation again, it might mean that I need to check every symbol on a path to a final state?
Yes, I mean every symbol on a path to the final state.
-- Eric

LordHoto
BASIC-Programmierer
BASIC-Programmierer
Beiträge: 135
Registriert: 14. Dez 2009 17:00

Re: Orphan Shadow Analysis

Beitrag von LordHoto » 28. Feb 2012 14:19

ericbodden hat geschrieben:
LordHoto hat geschrieben:Or do I understand the "for every symbol that is required to reach a final state" wrong, on a first read it sounded to me like this really means just all the symbols which directly enter a final state from *any* other state. But reading your explanation again, it might mean that I need to check every symbol on a path to a final state?
Yes, I mean every symbol on a path to the final state.
Ah thanks, that really clears up the confusion on my side then!
Compiler 1 Tutor WS 12/13

Antworten

Zurück zu „Automated Software Engineering“