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


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 {(xi, yi), i = 1, ..., n}. The function that describes x and y is:

yi = α + βxi + ε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(α, β) = ∑ni=1ε^ 2i = ∑ni=1(yi - α - βxi)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

LR Args

LR Args

where rxy is the sample correlation coefficient between x and y; sx is the standard deviation of x; and sy is correspondingly the standard deviation of y.