feature/sym: shape checking tooling for DiffSharp#207
feature/sym: shape checking tooling for DiffSharp#207dsyme wants to merge 19 commits intofeature/gmodelsfrom
Conversation
Codecov Report
@@ Coverage Diff @@
## feature/gmodels #207 +/- ##
===================================================
- Coverage 65.26% 59.33% -5.93%
===================================================
Files 29 28 -1
Lines 6664 7350 +686
Branches 1573 1669 +96
===================================================
+ Hits 4349 4361 +12
- Misses 1472 2147 +675
+ Partials 843 842 -1
|
|
Some sample symbolic shape inference, for example the Conv2DTranspose model: gives This is correctly inferring that the D,H,W of the output is the same as the input, and the C of the model must match the C of the input, and verifies that the outChannels of the model is the outChannels of the input. All very nice. In the above the kernelSize is an optional parameter and is actually 1. If we want to include optional kernelSize, strides and paddings: gives: Note that the full (and quite complicated) shape type of the model's forward function has been inferred automatically from the implementation (by running the symbolic ShapeChecking backend, collecting constraints and solving with Z3). (In the above hint is actually needed for the names N,C,H,W though that should really be reported by the model I think. ) |
|
Live shape checking tooling - concrete or symbolic - working on DiffSharp models. After discussion with @gbaydin this is with almost no adjustment to the model code, just
Modified VS tooling and Will make more samples and documentation in due course. But this thing actually works, it's quite amazing. |
f96f999 to
a5d2213
Compare
Foundations for shape checking and inference, discussed with @gbaydin today
see #274 for more details
Quick guide to the design and implementation
DiffSharp.Core:
Shapes are potentially symbolic
Int[]. HereIntis a potentially symbolic integer. The cost is one extra word on theIntstruct and one extra word on theShapestruct, there are implementations of no-cost non-symbolicIntandShapeunderNO_SYMBOLIC_SHAPEdefine in the codebase if we ever need to trim this back.For a core operator, constraints are generated during tensor execution (eg with ShapeChecking backend) via a
Shape.checkXYZcall which is implemented as a series of checks which generate constraints, see also here and hereThese constraints are not processed directly by DiffSharp.Core but are rather emitted via a sink ISymScope attached to any symbolic shapes encountered. If no symbolic shapes are present (as in normal tensor execution) then no
ISymScopeis needed.Internally in Tensor.fs and RawTensor.fs the
Shapetype is used (e.g.member internal tensor.conv2dx). In the default public API you get viaopen DiffSharp, i.e.Tensoranddsharp.*, shapes areint[]. There is essentially no change to the external API.Parts of the external API are replicated and adjusted with potentially-symbolic shapes in
open DiffSharp.ShapeChecking. Users can use this if they want the option of full symbolic shape checking, e.g. w.r.t. symbolicstride,padding,dialation, tensor indexing and so on. The use this API is not always necessary though - you can shape check with non-symbolic shapes without this, and even some symbolic shapes e.g. on inputs.tools/DiffSharp.ShapeChecking:
When using shape checking tooling of any kind, symbols of can be injected into execution as part of tensors or their shapes, or any
Intvalue. Here is the implementation of the symbol type when shape checking tooling is active, basically just a Z3 expression. Note we are now in "tools" - this is only active when doing shape checking. The constraints flowing out of DiffSharp.Core are mapped to Z3 constraints and here is where they are checked by Z3 and here is where we give nice formatting to Z3 expressionsShape checking tooling of any kind sets the default backend for DiffSharp to the shape checking backend where tensors only carry shape, element type and device information. The shape checking tooling switches the default backend via setting an environment variable prior to execution.
Shape checking tooling can now be programmed up however we like - at minimum it needs to be connected to the programmer front end. This can for example just be a command line invocation, e.g. to analyse code using reflection and print a report. This was the first thing I prototyped and you can imagine many such tools.
For such reflective analysis, the symbols pumped into the code for each argument depend on the attributes and types and a small parser for symbolic shape annotations
When using shape checking tooling in conjunction with the VS IDE, the ShapeCheckAttribute is used to trigger dynamic interpretation of code in shape checking mode. Only the shape checks are run. The
fslive.exetool knows about this attribute and how to call itsInvokemethod with the right data. It runs in the background and hands its results over to the VS IDE for hover tips and error diagnosticsThe end result is that the shape checking tooling runs your code as you type in a special "live check, shape check" mode using a restricted form of execution, with attention to generate good hover tips and diagnostics