[Question]Abstract Interpretation for proving liveness property

[PSuHyeon]

While studying for final exam, I get to have question about abstract interpretation for proving liveness property.

As we learned in the class, abstract semantics soundly subsume all semantics defined in concrete semantics.

In addition, abstraction for values (such as integer or memory) soundly subsume, and may over-approximate, the concrete values that might occurs during the execution of program.

However, when we have to prove the existence of some property, not the absence of some property, having sound subsuming semantics becomes unsound. (I thought this way because to soundly prove existence of some property, we have to under-approximate such property. (i.e, if it is not sure if the property exists or not, say there is no such property.))

And my conclusion was that the abstract interpretation can be used to completely prove liveness property, while it is not possible to soundly prove the liveness property.

My question is

1. Can abstract interpretation framework soundly prove liveness property?
2. If yes, does abstract semantics operators and values still has to subsume all concrete semantics operators and values?

Actually, I had this question while solving past exam question: Password-486 in 2021. It seems like property defining certified program is liveness property, not safety property.

[KihongHeo]

Hi,
Good question.

First, my intention was to ask students to design an analyzer NOT for liveness property, but for safety property, as you folks did in the homework. Since it is impossible to make a sound and complete analyzer, either of the following is ok in practice:

1. Whenever the analyzer says "certified", the program is truly certified,
2. Whenever a given program is truly certified, the analyzer says "certified"

This is the same as our homework:

1. Whenever the analyzer says "no-division-by-zero" (i.e., no alarms), the program is safe from DBZ, (<== our homework)
2. Whenever a given program is safe from DBZ, the analyzer says "no-division-by-zero"

We chose the first option to detect division-by-zero bugs in the homework. Similarly, you can design an analyzer for detecting password-486.

I think you got confused with the following two things:

• the soundness of the proof system (i.e., the analyzer says "certified" then truly certified)
• the soundness of the abstract semantics (i.e., the abstract semantics subsumes the concrete semantics)

In the problem, by soundness, I mean the second one.

BTW, the abstract interpretation framework can be used to prove liveness properties. The basic principle is the same (i.e., soundly subsumes all the concrete behavior). However, the domain designs in the lecture are not appropriate for liveness properties. Consider termination analysis using the interval domain in the homework. We interpret the analysis results as follows:

• if the output of the program is $\bot$: this program definitely does not terminate.
• if the output of the program is $[1,1]$: the program may not terminate or returns 1 "if terminates"
• if the output of the program is $[1,10]$: the program may not terminate or returns 1,2,3,...,or 10 "if terminates"

See the problem. Our abstract domain is not able to represent this kind of information "this program definitely terminates and returns 1,2,3,..., or 10". For termination analysis, you need to design a new abstract domain. For example, $Itv \cup \lbrace !, \bot, \top \rbrace$. With this domain,

• if the output of the program is $!$: this program definitely does not terminate.
• if the output of the program is $[1,1]$: the program definitely terminate AND returns 1
• if the output of the program is $[1,10]$: the program definitely terminate AND returns 1,2,3,...,or 10
• if the output of the program is $\top$: the program may or may not terminate

[PSuHyeon]

Thank you so much for great detailed explanation!

I have follow up questions regrading soundness.

There are two soundness according to above explanation:

• the soundness of the proof system (i.e., the analyzer says "certified" then truly certified)
• the soundness of the abstract semantics (i.e., the abstract semantics subsumes the concrete semantics)

I thought second soundness is required to achieve system with first soundness. (Abstract semantics 를 안전하게 디자인 하는 이유가 분석기의 최종 결과를 안전하게 위함이라고 생각했습니다.)

However, for this problem, soundness of abstract semantics leads to unsoundness of analyzer.

For example if we were to find if variable x hold 486 at any time in program:

void f(){
 ...           // y = [400, 500] (y = 450 in actual execution)
x = input();      // ignore the case x being Top so that it include 486.
if(x < y){
   x++;        // x = [-oo, 500] 
}

analyzer would says yes since 486 is in the range of x. However, in real execution, value of x would not be 486. Therefore, analyzer is saying 'certified' for not certified program, so it is not sound.

So I am curious how could sound abstract semantics leads to unsound analyzer.

Also, for properties of certified program:

• A certified program has at least one integer variable (say, x) at some point of the program such that x mod 2021 = 486.

if I change point when at least one integer variable having x mod 2021 = 486 as termination, it becomes termination problem. Can you explain how this property can be interpreted as safety property?

Again thank you so much in advance for answering. I am worried if my question is so exam question specific. Second question can be ignored in such case.

[KihongHeo]

This is what people usually get confused about.

1. "Soundness" is not something absolute. It always accompanies "with respect to X". So the two soundness statements are independent of each other:

• (first) the proof system is sound with respect to the certification
• (second) the abstract semantics is sound with respect to the concrete semantics

Here the intention is the second one.

2. Soundness and completeness are two sides of a coin. If you design your analyzer as above, then you can achieve a sound proof system with respect to "not-certified-program detection". Whenever your analyzer says "Yes. This is dangerous", it is true. (Do not assume we always prove good things!).

3. In your example, the analyzer results say "may be certified". But it is ok. Static analyzers can produce spurious answers.

4. Similar to (2), you can prove "non-termination" rather than "termination".

void f() {
    while(true) { skip }
    // you HW analyzer will give bottom here
}

Your homework analyzer will conclude the non-termination, also it is truly a non-terminating program. Of course, there will be a non-terminating program for which your HW analyzer says "may terminate":

void f() {
    while(*) { skip } // non-terminating loop with a very complicated condition
    x = 486
}

Your homework analyzer will say "it may terminate and produce 486". It is a sound abstract interpretation because it subsumes the concrete semantics. Also this analyzer is a sound proof system for "non-termination". (but failed to prove non-termination for this example)

[PSuHyeon]

Oh now I understand how soundness can be interpreted differently based on its subject. Soundness could be completeness in another perspective and completeness could be soundness in yet another perspective. Thank you for answering question!🙂