2 definitions
2.1 General Idea
Before we can start proving properties about our actual mathematical object we first need to actually start writing down what our definitions are. Thus what we aim to do here is write down all the definitions we require.
2.2 Speedup function
coreSpace is defined to be the actual allowed allotment of cores i.e. if given a vector \(c \in \mathbb {R}^n\) describing how many cores we have then our corespace becomes: \(x \in \mathbb {R}^n\) with the requirement that: \(0 \leq x_i \leq s_i\) forall \(1 \leq i \leq n\). After this we shall abbreviate this space as \(C_c\).
The Mathlib library already defines concavity more generally. We redefine our own instance to make it easier to work with:
A function \(f\) is said to be concave on \(c \in \mathbb {R^n}\) the core vector if \(\forall x, y \in C_c\) and all \(a, b \in \mathbb {R}\) with the property that \(a + b = 1\) implies that:
A function \(f\) is said to be sublinear on \(C_c\), with \(c\) the core vector if \(\forall x \in C_c\) \(||f(x)|| \leq ||x||\).
This brings us to the definition of the speedup function:
A function \(s \colon C_c \to \mathbb {R}\) is said to be a speedup function if \(s\) is concave and sublinear on \(C_c\).
2.3 Markov Chain definitions
Since our queue will be one-dimensional of infinite size anyway we define our RateMatrix to be the following:
A function \(Q \colon \mathbb {N} \times \mathbb {N} \to \mathbb {R}\) is said to be a rate matrix if the following holds:
\(Q(0,1) = -Q(0,0)\)
\(\forall n \in \mathbb {N} \neq 0, Q(n, n+1) + Q(n, n-1) = -Q(n,n)\)
\(\forall n, k \in \mathbb {N}, |k-n| \geq 2, Q(n,k) = 0\)
Now the invariant distribution of our queue is simply:
An infinite-dimensional vector lambda described by a function \(\mathbb {N} \to \mathbb {R}\) is said to be an invariant distribution for a queue \(Q\) if the following holds:
\(\forall n \in \mathbb {N}, n \neq 0, \lambda (n-1) * Q(n-1,n) + \lambda (n+1) * Q(n+1,n) = \lambda (n)\)
\(\lambda (1) * Q(1,0) = \lambda (0)\)
\(||\lambda ||_1 = 1\).
We will define the mean response time of our queue directly dependent on Little’s law, since the only way we evaluate our mean response time is by invoking Little’s law anyway.
The mean response time, denoted as \(\mathbb {E}[T]\) of a queue is defined to be the mean number in the system / mean throughput i.e. (mean throughput is equal to \(\Lambda \) since this doesn’t vary per state):
2.4 Scheduling Policy
Now we have everything we need to state what a policy is. For this we first define what a policy is.
A policy is a function \(p \colon \mathbb {N} \times \mathbb {N} \to \mathbb {R}^n\) describing per state \(n\) how to allocate cores in \(C_c\) over \(j\), \(0 \leq j \leq n\), jobs. Thus if we write this out, \(p\) is subject to the following conditions:
\(p(n,j) = 0 \forall j {\gt} n\).
\(\left(\sum _{k=0}^i p(i, k)\right) \in C_c\)
\(\forall 0 \leq i \leq n, p(n,i) \geq 0\)
Now we can define the magnum opus of our actual definitions: the schedule policy.
A schedule policy is a function describing for a specific queue \(Q\) and a specific speedup function \(s\) the departurerates per state \(n\).