## 2014-11-19

Published on 2014-11-19## Godson-T murphi-modeling (2)

### Model Rules in Godson-T

As we mentioned, all rules that need replace cached data to memory should be separated into two parts in our murphi model, which is inspired by interrupts in systems programming or function calls in programming languages. The two stages are listed as follows:

- Firstly, save current state to the
*assistant variables*such as`curNode`

,`curCache`

, etc. Then*REQUIRE*the replacement. - Secondly, after the replacement has been
*DONE*, retrieve the stored states and resume the interrupted rules, and set the replacement state to*NON*.

There are also some tips we should keep careful.

- All normal rules except replacement stages and resumed stages, must be triggered under the condition that the replacement state is
*NON*. - All resumed stages must be triggered under the condition that the replacement state is
*DONE*. - The replacement state must be asserted in every
*guard*part of each rule including invariants. - If need to assert cache state and cache content, cache state must be asserted first.
- If need to assert attibutes of locks, the
*beUsed*attribute must be asserted first.

The last three tips can be ignored if we initialize all variables in the start state.

### Deal with Counterexamples

#### Properties

There are two properties that the cache coherence protocol must hold.

**Deadlock-free Property**: One node can only hold one lock at the same time.**Coherence Property**: The cached data must be the same with data in their associated memories. In Godson-T, this means*Read*operation in*critical region*must cache correct data.

#### Counterexamples and Solutions

With those *strong* properties above, our model will generate a *counterexample*, which implies that two different *process* could cache the same location of memory in critical region protected by different locks, and once one of them modified the memory (with *write through* strategy), the other would cache wrong data.

There are two solutions to this problem.

- Do not allow multiple locks, e.i., there is only one lock there
- Weaken the
*Coherence Property*, so as to permit the counterexamples, and only require that the cached data must be correct in which critical region protected by the same lock.

## Linear Regression

*Simple Linear Regression* is the *least squares* estimator of a linear regression model with a single explanatory variable. In other words, simple linear regression fits a straight line through the set of *n* points in such a way that makes the sum of squared *residuals* of the model (that is, vertical distance between the points of the data set and the fitted line) as small as possible.

Suppose there are *n* data points {(*x _{i}*,

*y*),

_{i}*i*= 1, ...,

*n*}. The function that describes

*x*and

*y*is:

*y _{i}* =

*α*+

*βx*+

_{i}*ε*.

_{i}The goal is to find the equation of the straight line which would provide a "best" fit for the data points. Here the "best" will be understood as in the least-squares approach: a line that minimizes the sum of squared residuals of the linear regression model. In other words, this is a minimization problem:

Find minimum *Q*(*α*, *β*) in *α* and *β*, for *Q*(*α*, *β*) = ∑^{n}_{i=1}*ε*^{^ 2}* _{i}* = ∑

^{n}_{i=1}(

*y*-

_{i}*α*-

*βx*)

_{i}^{2}.

By using either calculus, the geometry of inner product spaces, or simply expanding to get a quadratic expression in *α* and *β*, it can be shown that the values of *α* and *β* that minimize the objective function *Q* are

where *r _{xy}* is the sample correlation coefficient between

*x*and

*y*;

*s*is the standard deviation of

_{x}*x*; and

*s*is correspondingly the standard deviation of

_{y}*y*.