How it Works

Compilation and execution of a Delite program occurs in three separate stages:

Compile-time (done by build-cvx script)

check program syntax and compile Scala sources
produce executable code that is run at staging-time

Staging-time (done by delitec script)

convert DSL program into an abstract-syntax tree
generate code in the target language (usually Scala)

Walk-time (done by delite script)

compile the generated code (using a standard compiler for that language)
run the code

For any given program, all of the steps before running the code may only be done once (so one may think of them as analogous to "compiling" in other languages). OptiCVX does as much processing as possible at staging-time, in order to improve performance. In particular, it does the following:

Verify disciplined convex programming (DCP) rules are followed
Convert the user program into one or more standard-form conic programs using rewriting rules
Emit code for a solver that will operate on this conic program, given the user's input data known at runtime
Emit code to send data to and from the solver, and to connect it to the rest of the program

We will look at how the DSL accomplishes each of these tasks below.

DCP Rule Verification

OptiCVX formalizes DCP rules using a datatype called a "signum". Simply put, a signum (an element of the set of signums) formalizes the notion of the sign of an expression. (We can also think of it as the set of cones on the real numbers.) There are only four possible signums: "zero", "positive", "negative", and "all". The seemingly-disparate value "all" is used to denote a situation where any sign is possible. Note also that the "positive" and "negative" signums both admit the possibility of a zero-valued expression. (Strictly, they should be called "nonnegative" and "nonpositive", but this would be tiresome).

Signum objects naturally admit a notion of binary addition, multiplication, and negation (although negation does not produce the additive inverse, as the signum set is not a ring). Furthermore, it naturally admits an ordering which formalizes the notion of "is a" on this set; e.g. zero < positive because any zero-valued expression must also be nonnegative.

We associate signums with vexities in the following way:

Zero with an affine expression
Positive with a convex expression
Negative with a concave expression
Any with no known vexity information

Similarly, we associate signums with monotonicities in the following way:

Zero with a constant function
Positive with a nondecreasing function
Negative with a nonincreasing function
Any with no known monotonicity information

We also assign a signum value to constant scalars, as follows:

Zero with a scalar known to be zero
Positive with a scalar known to be nonnegative
Negative with a scalar known to be nonpositive
Any with a scalar with no known sign information

Using this framework, we can formalize the rules that we want to enforce. Letting A and B be expressions, c be a constant scalar, f be some function, V(...) denote the vexity (as a signum), Mx(...) denote the monotonicity of the function in the x-th argument (as a signum), and S(...) denote the sign (as a signum), then the DCP rules become simply:


            V(A+B) := V(A) + V(B)
            V(-A) := -V(A)
            V(c*A) := S(c)*V(A)
            V(f(A1,A2,...,An)) := V(f) + M1(f)*V(A1) + M2(f)*V(A2) + ... + Mn(f)*V(An)

As a base case, we let all variables declared by the user be considered affine. This process allows us to recursively assign a vexity to all of the expressions used in the DSL. To do verification, we require the following:

Any expression to the left of a "<=" must be convex, and any expression to the right must be concave
Any expression being constrained to lie inside any higher-dimensional convex cone must be affine
Any expression being minimized must be convex, and any expression being maximized must be concave

We note here that any non-scalar expression will always have vexity affine, since it is impossible for a vector-shaped expression to be convex or concave. We could potentially extend this system to handle higher-dimensional analogues to convexity (starting by defining a higher-dimensional signum type that corresponds to the set of cones in a particular dimension), but since the DCP rules used in CVX do not do this, it has not yet been investigated.

Conversion to Standard Form

Conversion to standard form is actually very straightforward. The DSL provides five basic statements that can be used to describe problems. These are:

constrain_zero(...)
constrain_nonnegative(...)
constrain_secondordercone(...)
constrain_semidefinite(...)
minimize (...) over (...)

        

Other operations, such as the == and <= constraints, are implemented as syntactic sugar on top of these fundamental operations. Now, to convert a problem to standard form, we basically do the following: whenever we encounter a constraint, we push that constrain onto a list of constraints for each of the variables that is effected by that constraint. Then, when a minimization statement is encountered, we gather all the constraints that act on the variables being minimized over and produce their Cartesian product to create a problem of the form:


minimize c^T*x
  over x ∈ Rⁿ
  subject to
    A*x + b = 0
    F*x + g ∈ K
  for some matrices A and F, vectors b, c, and g, and symmetric cone K.

Of course, since this is staging time, the matrices and vectors are not known. Indeed, even their size can vary. What the DSL generates is an abstract syntax tree that can later be compiled to perform matrix-vector multiplications. This can be thought of as akin to a sparse matrix. The symmetric cone K is just a product of some number of simplex, second-order, and semidefinite cones (although the sizes of these cones are not known at staging-time, the number of cones is known).

In order to deal with functions, the DSL basically just runs the body of the function, accumulating all variable declarations, constraints, and minimizations. It then adds these to the main problem. Thus, all OptiCVX function invocations are effectively inlined.

OptiCVX recognizes when a minimization statement is only a partial minimization, and does not instantiate a solver if this is the case. It will only create a solver, and allow variable resolution, if no variable bound by the optimization statement is connected by a constraint to any unbound variable. This allows multiple different optimization problems to be run in the same program.

Emitting Code

For each problem above, OptiCVX currently emits an ADMM solver. The solver uses the LSQR algorithm for computing the ADMM step that requires projection onto the affine constraint. Both of these algorithms only require information about the matrices in the form of a method for matrix-vector multiplication, so they work well with our abstract-syntax-tree matrix representation. The solver runs at the time at which the minimization statement occurs.

The emitted code is based entirely off of the dense vector operations of the linear-algebra DSL, OptiLA. OptiLA's dense vector operations are a thin wrapper around Delite ops, and allow for code reuse for many functions, such as vector addition, that must be used across many DSLs. In addition to OptiLA, OptiCVX also uses the looping IR nodes included in LMS to enable the iteration of the solver. Since this encompasses the entirety of the operations performed by the DSL, OptiCVX does not itself emit any target code. This theoretically allows it to be easily retargeted at any platform supported by OptiLA's generators.

The results of the solver run are read out by using a resolve(...) statement. It is a staging-time error to try to call resolve before a solver has run. Presently, there is no way to access dual variables or determine whether the problem is feasible, but I plan to add these features.

Unfortunately, the code output by the stager is typically quite long and uninstructive, as it consists mostly of inlined for loops for all of the vector operations. Therefore, I have not here included an example of code emitted by the stager.