[GitHub] [tvm] FranckQC opened a new issue #9250: [Potential Bug] SSAVerifier needs some clarification and/or fix

[GitBox <gi...@apache.org>]

FranckQC opened a new issue #9250:
URL: https://github.com/apache/tvm/issues/9250


   Hi everyone,
   
   Following the discussion started [here](https://discuss.tvm.apache.org/t/tir-are-multiple-let-in-with-the-same-var-allowed-ssa/10881/6) I would like to discuss a thing that seems weird in the SSAVerifier implemented in verify_ssa.cc.
   
   The notion of SSA form that TVM implements is quite customized.
   
   **1)** The first thing to notice is that the SSA form that TVM is using rather strict : even in different contexts, variables must be different. That is perfectly ok and I understand that this makes things easier.
   For instance, with the code:
   
   ```
   let x = 10 in ...;      // A statement
   let x = 200 in ...;     // Another statement
   ```
   Even though these two `x` live in different contexts, this situation is forbidden.
   
   As already said, **that is perfectly fine because it is stricter than what we usually call SSA**. Said differently, when SSAVerifier returned true, it was really an SSA form. But that was only the case until Jun 28, 2020 and the commit 4fbfaca5fc, which made SSAVerifier weaker with a specific exception which I will now describe.
   
   **2)** The exception added a year ago by @tqchen is that a let-in expression (not a let-in statement!) can redefine a variable previously defined (in a let-in expression or let-in statement) if the variable is bound to "the same" value.
   That is even possible within the same context. This is described in [the code](https://github.com/apache/tvm/commit/4fbfaca5fc417b09330f7592b21efdc6fb1cf51b#diff-a473f155b7fda12e91373b0d8dcc7e5eb5aad3c96f67e69636453bf0d5ad487fR51-R62) as the "**Weaker SSA condition**".
   
   According to a comment in the code, it seems that this possibility was added in order to allow things like :
   `(let x = 1 in x+1) + (let x = 1 in x+1)`
   which seems needed for some passes "that reuse a single let-in expression for building a nested one".
   The fact that the passes vectorize_loop, split_host_device, simplify and loop_partition were modified by the same commit tells us that this exception is probably needed due to what these passes produce. But I haven't checked more precisely why exactly these passes produce such things.
   
   Anyway, **adding this exception could be fine (leading indeed to a weak-SSA form), but the way it is implemented is not:**
   
   The problem with the way this exception is implemented is that it allows such redefinition if the variables are defined with "the same" value. But this notion of "the same" is implemented using ExprDeepEqual which checks that the two expressions are **syntactically** the same. But such a syntactic check will be too weak here, as function calls and memory loads can be syntactically the same but can reduce/compute to different values.
   
   Think about:
   `(let x = f(y) in x+1) + (let x = f(y) in x+1)`
   SSAVerifier will answer true here, but **this code is not weak-SSA** as `x` can contain different values if the function `f()` does not always return the same value for the same inputs (ie if `f()` does side-effects like reading the memory).
   
   **3)** Note that we also have this problem with memory loads. 
   
   For instance:
   
   ```
   let x = Mem[i] in ...;              // A statement initially defining x
   Mem[i] = newVal;                    // Changing the content of the memory Mem[i]
   ... (let x = Mem[i] in x+1) ...     // An expression redefining x with syntactically the same value
   ```
   
   Again, SSAVerifier will answer true here, but **this code is not weak-SSA** as `x` can contain different values!
   Therefore, here again, checking only the syntactical equality is too weak.
   
   ### Suggestions for fixing this issue
   
   - 1. We first need to make sure that this weak SSA form is indeed still needed for convenience because of some TIR passes that produce code like that. Could you please confirm on that please?
   
   - 2. If this exception is indeed still needed, we just need to make it a little bit more restrictive : variables defined with a value that contains function calls and/or memory loads should not be allowed to be defined several times (even if their definitions is syntactically the same!).
   
   I would be very happy to provide more details and even to fix this issue if you think that what I'm describing here is correct. If you have some time to have a look at this @tqchen and to conform what I said that would be very appreciated :). I can do the fixing myself without problem but I just need to conform first.
   Many thanks in advance!
   
   If you want to try things out, you can try with the code I have already given in the [discussion](https://discuss.tvm.apache.org/t/tir-are-multiple-let-in-with-the-same-var-allowed-ssa/10881/6) for testing the case of `(let x = f() in x+1) + (let x = f() in x+1)` which I'll copy here for convenience:
   
   ### Code to try  / Steps to reproduce
   
       RelayExpr fun = GlobalVar("fun");
       Array<PrimExpr> emptyArray;
       // Function call : f()
       Call call = Call(DataType::Int(32), fun, emptyArray);
   
       // 1 - What does ExprDeepEqual tells when comparing f() and f() ?
       ExprDeepEqual deep_equal_;
       if (deep_equal_(call, call))
       {
           std::cout << "Yes, f() is deeply equal to f()" << std::endl;
       }
       else
       {
           std::cout << "No, f() is NOT deeply equal to f()" << std::endl;
       }
   
       // 2 - What does VerifySSA tells on (let x = f() in x+1) + (let x = f() in x+1)?
       Var x("x");
       // Let x = f() in x
       Let let1 = Let(x, call, x);
       // Let x = f() in x
       Let let2 = Let(x, call, x);
   
       // (Let x = f() in x) + (Let x = f() in x)
       PrimExpr sum = Add(let1, let2);
   
       Var buffer("Mem");
       Var i1("i1");
       // Mem[i1] = (Let x = f() in x) + (Let x = f() in x);
       Stmt progStmt = Store(buffer, sum, i1, IntImm(DataType::Int(32), 1));
   
       // Just a main function calling progStmt
       Array<tir::Var> emptyVars;
       PrimFunc prog = PrimFunc(emptyVars, progStmt);
   
       if(VerifySSA(prog))
       {
           std::cout << "Handwritten prog is SSA!" << std::endl;
       }
       else
       {
           std::cout << "Handwritten prog is NOT SSA" << std::endl;
       }
   
   
   ### Expected behavior
   
   This code should print : 
   
   "Yes, f() is deeply equal to f()
   Handwritten prog is NOT SSA"
   
   ### Actual behavior :
   
   This code actually prints :
   
   "Yes, f() is deeply equal to f()
   Handwritten prog is SSA!"
   
   ### Environment
   
   Using latest TVM in main branch
   
   Many thanks again!
   


-- 
This is an automated message from the Apache Git Service.
To respond to the message, please log on to GitHub and use the
URL above to go to the specific comment.

To unsubscribe, e-mail: commits-unsubscribe@tvm.apache.org

For queries about this service, please contact Infrastructure at:
users@infra.apache.org

[GitHub] [tvm] tqchen commented on issue #9250: [Potential Bug] SSAVerifier needs some clarification and/or fix

[GitBox <gi...@apache.org>]

tqchen commented on issue #9250:
URL: https://github.com/apache/tvm/issues/9250#issuecomment-944911597


   Thank you for bringing this up!  Indeed we will need to make the condition stronger here such that under a weak ssa form, we would require the related expressions to do not call into function that have side effect or write into a state.
   
   Note that by default store have to appear in a Stmt so the case of memory write won't interleave with the two lets
   
   You are right that it is also think about whether or not such form was indeed necessary. The let expr is useful when it comes to express values that are CSEed.
   
   In the case of TIR, we do want to restrict where can effectful operations appear(hopefully in let statement, or eval) so the impact is minimized and most Expr can remain pure.


-- 
This is an automated message from the Apache Git Service.
To respond to the message, please log on to GitHub and use the
URL above to go to the specific comment.

To unsubscribe, e-mail: commits-unsubscribe@tvm.apache.org

For queries about this service, please contact Infrastructure at:
users@infra.apache.org