Added documentation for SSA like property in Bufferization.

[dfki-jugr]

Summary

Added additional information about the SSA like properties
that has to be fulfilled in the bufferization steps.

[silvas]

mlir/docs/BufferDeallocationInternals.md

33

I found this wording confusing (such as the term "full buffer write"). I would suggest to just say that all writes to a memref introduced by bufferization must dominate all reads (you say this below in a parenthetical but it should be the primary definition of the constraint).

[silvas]

mlir/docs/BufferDeallocationInternals.md

33

And strictly speaking, I would say that all writes must dominate all tensor_load ops. I think it is okay to read and write arbitrarily before the tensor_load.

E.g. this is fine, despite having intermixed reads and writes:

%0 = alloc()
store %0[0] = 42
%1 = load %0[0]
%2 = add %1, 7
store %0[0] = %2

[silvas]

mlir/docs/BufferDeallocationInternals.md

33

For example, the bufferization of linalg.matmul effectively results in load/add/store similar to the above.

[herhut]

mlir/docs/BufferDeallocationInternals.md

33

I found this wording confusing (such as the term "full buffer write"). I would suggest to just say that all writes to a memref introduced by bufferization must dominate all reads (you say this below in a parenthetical but it should be the primary definition of the constraint).

As you mention yourself, this is not true for bufferization patterns that iteratively produce their value. So this is not good enough either. The goal of this restriction in essence is to ensure that if we need to insert a copy for an allocation as it escapes, we need to be sure that we do not hide mutations. If the allocation dominates all writes, then a copy should never be needed. I have not thought this through, though.

And for bufferization patterns, we would have the requirement that they may only write to buffers they allocated themselves.

[herhut]

I think we should land this as it is strictly an improvement over the current documentation. We can improve further but having it documented avoids more confusion than it creates.

mlir/docs/BufferDeallocationInternals.md

 `RegionBranchOpInterface` to model inter-region control flow.
 * Terminators yielding values to their parent operation (in particular in the
 scope of nested regions within `RegionBranchOpInterface`-based operations),
 should implement the `ReturnLike` trait to represent logical “value returns”.
 
 Example dialects that are fully compatible are the “std” and “scf” dialects
 with respect to all implemented interfaces.
 
+During Bufferization, we convert immutable value types (tensors) to mutable
+types (memref). This conversion is done in several steps and in all of these
+steps the IR has to fulfill SSA like properties. The usage of memref has
+to be in the following consecutive order: allocation, write-buffer, read-
+buffer.
+In this case, there are only buffer reads allowed after the initial full
+buffer write is done. In particular, there must be no partial write to a
+buffer after the initial write has been finished. However, partial writes in
+the initializing is allowed (fill buffer step by step in a loop e.g.). This
+means, all buffer writes needs to dominate all buffer reads.
+
+Example for breaking the invariant:
+
+```mlir
+func @condBranch(%arg0: i1, %arg1: memref<2xf32>) {
+  %0 = memref.alloc() : memref<2xf32>
+  cond_br %arg0, ^bb1, ^bb2
+^bb1:
+  br ^bb3()
+^bb2:
+  partial_write(%0, %0)
+  br ^bb3()
+^bb3():
+  "linalg.copy"(%0, %arg1) : (memref<2xf32>, memref<2xf32>) -> ()
+  return
+}
+```
+
+The maintenance of the SSA like properties is only needed in the bufferization
+process. Afterwards, for example in optimization processes, the property is no
+longer needed.
+
 ## Detection of Buffer Allocations
 
 The first step of the BufferDeallocation transformation is to identify
 manageable allocation operations that implement the `SideEffects` interface.
 Furthermore, these ops need to apply the effect `MemoryEffects::Allocate` to a
 particular result value while not using the resource
 `SideEffects::AutomaticAllocationScopeResource` (since it is currently reserved
 for allocations, like `Alloca` that will be automatically deallocated by a