Category: state maps

Categories
state maps

Trees in informal methods

What’s a tree? First define a sequence or length n> 0 as a total map s: {1,.. n}→ X. Let Nil be the empty sequence.  If s is a sequence of length n, and x is an element, then u = sx is the sequence of length n+1 so that u(n)=x and for i < n, u(i)=s(i). That is sx is the sequence obtained by appending element x to sequence s on the right. If X is a set, let X* be the set of finite sequences over X, the minimal set that includes Nil and sx so that if s is an element of X*, sx is also an element. If s is a sequence, then either s=Nil or s = ux for some sequence u that has a length one less than the length of s. Define the predecessor of a sequence by Pred(Nil)=Nil and Pred(ux)=u.

A tree is a map  T: X* → Y where whenever T(s) is defined, T(Pred(s)) must be defined. Note that T(Nil) must be defined if T is defined on any elements of X* at all.

Let V  the set of vertices contain exactly those elements s of X* so that T(s) is defined.  If V is not empty, Nil is in V and call Nil the  “root”. Let E the set of labeled edges consist of exactly all triples (s,x,sx) where T(sx) is defined. Then (V,E) is the standard graph theoretic definition of a tree.  Suppose, on the contrary that (V,E) is a tree with labeled edges, that is it is a undirected graph that is connected but has no cycles. Then define T(Nil) = root and T(sx) = v s.t. there is an edge labeled x from T(s) to v.

 

So a sequence is a map from numbers to elements and a tree is a map from sequences to elements.

 

Categories
state maps

Linked lists

What’s a linked list?

  1.  Let V be a set of values and A be a set of “addresses”.
  2. Say a map f is a “linked list element” compatible with values V  and addresses A if and only if f(value)∈ V and f(next) ∈  A. A linked list element map can have an arbitrary additional domain – we don’t specify that here.
  3. Let L: A→ X where X is a set of  linked list elements compatible with V and A.  L associates addresses with linked list elements.
  4. Given any a ∈ A we want to be able to trace the linked list with “a” as the head element. Define E(L,a,0) = a and  E(L,a,n+1) = (L(E(L,a,n)))(next).  The expression (L(E(L,a,n)))(next) can be unwrapped to understand it better (L(E(L,a,n)))(next) = (L(a’))(next) where E(L,a,n) = a’. Then (L(a))(next) = f(next) where L(a)=f is a linked list element. So the final value is some a”, an element of A.
  5. Say (L,a) is a linked list iff for every element a’∈A s.t. L(a’) is defined,  there is some non-negative n so that E(L,a,n) = a’
  6. Say (L,a) is a circular linked list iff it is a linked list and for some n, E(L,a,n+1) = a.

Finite sequences of length n>0 can be represented mathematically as maps u:{0, … n-1}→ Y for some set Y.   If  (L,a) is a circular linked list, define u(0) = L(a)(value) and  u(n+1) =  L(E(L,a,n+1))  if E(L,a,n+1)=  a, and undefined otherwise.

 

Categories
academics state maps systems

informal methods applied to networks and timeouts

Distributed computation involves many interesting issues concerning shared data. Here I want to sketch out what networks look like using applied (informal) mathematics so we can look at some algorithms for consensus and data consistency. No  formal methods or category theory or metamathematics of any kind have been used in making this note.

Start with a set M of messages and a set S of “sites” or site identifiers. We have a map  sources:M → S so that each message m is associated with the site that sent or can send it. We have two interesting subsets of M, Requests ⊂ M and Responses ⊂ M with Requests ∩ Responses = emptyset.  The idea is that some sites will send requests to other sites and may get responses back. Each response should be unambiguously associated with a request so there is a map req:Responses → Requests where, for m in Responses,  req(m)  is the corresponding element of Requests .

A network can be described as a collection of connected state machines that represent network sites or nodes. In this work, state machines are represented by maps f:E∗ → X where E is an alphabet of events, E∗ is the set of finite sequences over E, and f(σ) is the output in the state reached by following sequence σ from the initial state.  Let Null be the empty sequence so f(Null) is the initial state output. Write  (σ after a) for the sequence obtained by appending element “a” on the right of sequence  σ. The intuition is that  σ takes the system to the current state state and then an “a” event takes it to the state “after a”. For example, f(σ after a) > f(σ) means “a” caused the output to increase in value.

Sites can receive  messages, transmit  messages, and advance state just by the passage of a unit of time. Let  the set of events E include all the elements of M, each of which represents receiving that message, plus an event “transmit” which means – “transmit the message the site is attempting to send” – and “tick” which means some unit of time passed.    Here is a definition of a function to count how many times the site received any particular message.

  • RxCount(Null,m) = 0,
  • RxCount( σ after m, a) = RxCount( σ, m)+1 if  a=m
  • and  RxCount( σ after a, m) = RxCount( σ, m) otherwise.

We can also count the number of ticks since the first time a message was received.

  • TickCount(Null,m)=0,
  • TickCount( σ after a, m) = TickCount( σ,m)+1 if (a=tick AND Received( σ,m) >0),
  • TickCount( σ after a, m ) = TickCount( σ,m) otherwise

 

Suppose we have some state function tx so that tx(σ) =m when the site is attempting to transmit message m and tx(σ) =nil if the site is not attempting to send a message in the current state.  A transmit event causes  tx(σ) to be transmitted if tx(σ) is not nil.  Using tx as a parameter to a counting function, we get:

  • TxCount(Null,tx,m) = 0,
  • TxCount(σ after a,tx,m ) = 1+ TxCount(σ,tx,m) if a=transmit and m=tx(σ ),
  • TxCount(σ after a,tx,m ) = TxCount(σ,tx,m) otherwise.

We can also count how much time has passed since we first tried to transmit a message m.

  • TriedCount( Null, tx m) = 0
  • TriedCount( σ after a, tx m) = 1 if ( tx( σ) =m and TriedCount(σ, tx,m)=0
  • TriedCount( σ after a, tx, m) = TriedCount( σ,tx,m)+1 if (a=tick AND TriedCount( σ,tx, m) >0),

A “site”  s will be represented by two state dependent maps tx and g, with tx tracking transmits and g telling us whether the site has failed. We don’t specify what makes a site fail, only that it can fail and once failed, it never recovers (we can make this more smart, by specifying recovery actions later, but for now let failure be permanent).

(6) Let s be an element of our set of Sites and say (tx,g) represents site  s iff

  1.  tx(σ)in M or tx( σ) =nil
  2.  tx(σ)  in M implies source(tx( σ))=s
  3.  tx(σ) in Responses implies RxCount( σ, s,req(tx(σ))) > 0
  4.  g(σ) in {True, False} and  g(σ) implies ( tx(σ) = nil AND g(σ after a))
  5. EXISTS c> 0 so that for m in Requests where TickCount( σ, s,m) > 0 , for some r in Responses TriedCount( σ,tx,r)>0

The last requirement means that sites at lest have to try to send responses.

Suppose we have a set of such pairs (txs,gs) for s in S. The next thing to do is to determine a sequence of events σs  for each s in S because each site may “see”  a different sequence of events. That is, we need to specify a mapping from sequences σ that determine the state of the composite system (the network) and sequences σs determining the state of each component site s.

The network that contains all these sites can be itself represented as a state machine with its own event alphabet A and event sequences  σ over A.  At this point, we don’t have to know much about A, just about what happens to each σs when an event “a” is appended to σ  over A.  Let σs  = h(σ, s) and let h(Null,s) = Null so all sites start in the initial state. Then h(σ after a,  s) needs to be specified. For this system, each component can either advance by 0 or one step so

  • h(σ after a,  s)= h(σ,  s) or h(σ after a,  s)= (h(σ ,  s) after b) for some b in E.

The expression (h(σ ,  s) after b ) just means that b is appended on the right to the sequence h(σ ,  s). Now we need some rules for how the state changes in the sites relate to each other.  First, if time advances for one site, it has to advance for all of them:

  • h(σ  after a,  s) = (h(σ ,  s) after tick) implies that for all s’ in S,  h(σ  after a,  s’) = (h(σ ,  s’) after tick)

A message can be delivered to a site only if that message is sent by another site

  • h(σ  after a,  s) = (h(σ ,  s) after m) implies that h(σ  after a,  source(m)) = (h(σ ,  source(m)) after transmit) AND  txsource(m) (h(σ ,source(m))) = m

Notice that we don’t have to limit how many sites can transmit and receive or whether messages are broadcast or not. We could, alternatively require that h(σ  after a,  s) = (h(σ ,  s) after m) implies TxCount(h(σ after a ,txs,source(m)) > 0 to allow the network to deliver messages after a delay or out of order, but let’s start with something simpler.

Let Sent(σ,s,m)  be the number of times site s has sent message m and Recvd(s,m)  be the number of times site s has received message M.  A site s can be operating or failed  so let Failed(s) indicate that status.  Note σ in this context is the event sequence of the system (the network) and each   σs is the induced event sequence of site s.

  • Rcvd(σ, s,m) = RxCount(σs ,m)
  • Sent(σ, s,m) =  TxCount(σs,txs,m)
  • Failed(σ, s) =    gs(σs )
  • Since(σ, s,m) =    TickCount(σs ,m)
  • SinceTried(σ, s,m) =    TriedCount(σs ,m)

The network is loosely specified but has the properties that  (1) a site is either failed or not, (2) no message can be received unless it has been sent, (3) a site can only send a message if it is the source and (4) a response won’t be sent unless the corresponding request has been received by that site.

  1. Failed(σ,s) or not Failed(σ,s) . PROOF 6.4 and definition above.
  2. Recvd(σ,s,m) > 0 implies Sent(σ,source(m),m) > 0.  PROOF by definition and 6.3
  3. Sent(σ,s,m) > 0 implies source(m) = s. PROOF from the definition and 6.2
  4. Sent(σ,s,r)>0  for r  in Responses implies Recvd(σ,s,req(r))  PROOF from the definition and induction on sequence lengths.

For the network as specified, there is no boolean state function F and sites s and z so that F(σs) implies Failed(σ,z).That is, there is no way for any site to deduce the failed state of any other site.  Suppose there was such an F. Then for some σ we have F(σs ) and g(σz ). Let σ =concat(u,v) where u and v are sequences and u is the shortest prefix of σ  so that Failed(σ,z). There must be some such u or else Failed(σ,z) would be false. We can define a new (tx,g) that acts just like (txz,gz)  until after σ except that g never becomes true. Define g(w) = False for all sequences w and define tx(w)=  txz(w) whenever w is a prefix of σz (or equal to σz  ). If w has σz  as a proper prefix then set tx(w)=m for some arbitrary message m. Then replace (txz,gz) with (tx,g). In the new system F(σs ) is true but g(σz) is false and not only that, site z can send messages after site s has concluded that it has failed. Therefore no such F is possible.. This result is often called the Fischer-Lynch-Patterson Theorem.  To me, this result means the obvious: that without timeouts and some sort of message delivery probability, the network can’t guarantee anything much.

Now let’s informally state a property of the system that sites are obligated to try to respond to requests unless they fail.

  • .Recvd(σ,s,q) for q in Requests implies eventually either  Sent(σ,s,r) for some r so that q=req(r)  or  Failed(σ,s)

So what does “eventually” mean? Here is a property of sites.

  • 6.5.  EXISTS c>0 s.t. TickCount( σ, r) > c for r in Requests implies that (for some q, so that req(q)=r,  either (TxCount( σ, tx,q)>0) OR g(σ))

A site cannot force a response message to be transmitted, but it can try to transmit the response message and fail if its transmit request is ignored by the network for too long. Then we have a network property

  •  Recvd(σ,s,q) for q in Requests implies  ( Sent(σ,s,r) for some r so that q=req(r)  OR   Failed(σ,s) OR  Since(σs,s,q) < c ) where c is the bound from 6.5

 

Categories
state maps

Sorting and groups

Image result for permutation groupI can’t find much reference to this in the literature (see Maus for some hints and an interesting paper) , but surely people have looked at sorting as a problem in group theory? Given a sequence $latex s=[x_1\dots x_n] $ say a permutation $latex \pi$ sorts $latex  s$ if and only if $latex \forall 0 < i < n-1, x_{\pi i} \leq   x_{\pi(i+1)}$ — where we could use any partial order. So sorting becomes a problem of finding an element of the permutation group. If $latex s $ contains no repetitions, if $latex s_i = s_j$ only when $latex j=i$ then there is at most one element of $latex S_n$ that sorts the sequence. If $latex s$ is a sequence of one value, then every element of $latex S_n$ sorts the sequence. Maybe $latex n-  |\{x_i: 0 < i \leq n\}|$ tells us how many elements of $latex S_n$ sort $latex s$, but perhaps we have to differentiate between repetitions of a single value and repetitions of multiple values.  An element of $latex S_n, (i,j)$ corresponds to  a swap in $latex s$ – to

t := s(i); s(i) := s(j); s(j) := t;

so we could describe e.g. quicksort as a sequence of pairs.

Anyone have some references?

Categories
state maps

state equations in practice

 

When people think of mathematical models of state for programs and other computer systems, it’s natural and conventional to consider state as a map from symbolic names of state variable to values. This is an error for a number of reasons including, most critically, the lack of any compositional structure. Let’s step back and think about what a discrete state system looks like.

Notation warning: I’m using _ for subscript x_p or f_r or one_(two).

  1. Crucially, state changes in discrete steps, in response to “events” or “inputs” , so there should be a set E of discrete “events” called the event alphabet, The event alphabet defines all the possible events that can cause state to change. The event alphabet can be large or only partially known so we do not want to be forced to make it completely explicit at every stage of the specification.
  2. A finite sequence of events over E  can be thought of as a system history, describing what series of events drove the system from its initial state (which is the point at which no events at all had happened) to the current state reached by following the sequence from the initial state.  You could complain at this point that deterministic, single thread of execution (the sequence) models can’t describe non-determinism, parallelism, concurrency, and abstract properties, but you’d be wrong – keep reading. You might even, as many researchers in formal methods have done, argue that infinite sequences of events need to be taken into account.  That’s also not correct.
  3. Now we are going to take an odd step – I don’t want to start with a state machine or other object that represents the whole system. I want to start with state variables and state dependent functions that express some system property and how it changes in response to events. For example, a state variable Executing might tell us the process identifier of the currently running (executing) process or it could be set valued in a multi-processor environment. And  priority(p)  might be the priority of the process with identifier, p.  As the system advances state, the values of the state variable change but often we want to have properties that are true in any state. For example,    p in Executing and q in Waiting and priority(p) >  priority(q)  implies TimeSinceSwitch < t  would be a good property for some operating system that needs to schedule by priority but also let lower priority processes advance.
  4. The event sequence is a discrete state version of real variables like time for analog models of physical systems. State variables are dependent variables that depend on the event sequence and some map or collection of maps that extract  information from the event sequence.   Everything that determines current state is in the event sequence but state is not a completed thing, not an discrete object, it is the cumulative information of multiple state variables depending on that event sequence. The same event sequence may correspond to completely different collections of state variables for different systems.
  5.  We might have many state variables to specify how an operating system works or even how a simple gate works. Let’s think of all of them at the same level of abstraction as depending on the same event sequence (finite, of course).
  6. The key to this approach is to be able to compactly define state variables and abstract properties of state variables even though the event alphabets and maps on sequences of events will often be enormously complicated.
  7. Say a variable y is a state variable for an event alphabet E if  y=f(σ) for some function f where σ is a  finite sequence over E which includes the empty sequence Nil.  The map f is a solution for y  that extracts values from the sequence as state advances (as events are appended to the event sequence). Essentially y depends on two parameters: the sequence  and the map. These parameters are often implicit.
  8. By the definition of state variable, if y  is a state variable, then  y=f(σ)  for some f so y(z) = f(z)  by the usual convention.
  9. If y is a state variable then y(Nil) is the value of y  in the initial state since  y(Nil) = f(Nil).
  10. The convention here is that σ is always a free variable over E* (the set of finite sequences over alphabet E).
  11. If z is a sequence and e is an event or a variable over events, write z.e for the sequence obtained by appending e to z on the right.  So y(σ.e) is the value of y in the “next state” – the state after e – since y(σ.e) = f(σ.e). 
  12. If  y = y(σ.e) then the event “e” leaves the value of y unchanged.
  13. If y(σ.e) = y +2  then the event “e” increases the value of y  by 2. The equation  y(σe)=y+2 can be rewritten as f(σe)=f(σ) + 2 if we know f. 
  14. A primitive recursive definition on the sequence will completely define the solution f  if the recursive map is defined. So  [y(Nil)= k and y(σ.e) = h(e, y(σ)) defines f if h and k are defined.  Note y(Nil) = f(Nil)=k. And y(σe)= h(e,y) = h(e,y(σ)) = h(e,f(σ)). Suppose sequence w=<a,b,c>, then y(w) = f(<a,b,c>) = h(c,f(<a,b>)) = h(c,h(b,f(<a>)) = h(c,h(b,h(a,k)))).  In many cases we don’t want to or can’t specify f completely – f is a solution to the constraints on y and there may be many or infinitely many or no solutions.
  15. For example, suppose C is a state variable and C(Nil)=0 and C(σ.e) = 1+C(σ). Then we have defined C to be the length of the event sequence.
  16. Define L(σ.e) = e so L is the most recent event. We do not need to define L(Nil).
  17. Define [ SinceReset(Nil) = 0 and SinceReset(σ.e) = ( 0 if e=RESET and  1+ SinceReset otherwise).
  18. Suppose we have a state variable Clock that somehow determines time passed since initial state from the event sequence. Then (Clock(σ.e)- Clock) is the duration of event e in this state (and may be different for different values of  σ ). Define  waiting_p(Nil)=0 and waiting_p(σ e)=0 if Executing(σ e) =p and   waiting_p(σ e)= waiting_p+(Clock(σ e)- Clock)  otherwise. So  waiting_p is the time that process p has been waiting to become the executing process. We might want a property (waiting_p > k only if priority_p < priority_p where q = Executing).
  19. Ok, now we can consider component composition – which is just function composition. Consider the state variable L defined above and suppose we have a new alphabet B consisting of Left_x and Right_x for x in some set X of data values. The goal is to construct a shift register from n instances of L.  Define Li =  L(ui) where ui is also a state variable that has values that are sequences of elements of X. Usually we want components to state in the initial state so ui(Nil) = Nil.  This means Li (Nil)= L(Nil) which is something we didn’t define. Now define ui(σ e) where “e” is an element of the event alphabet of the composite system.  Remember I’m using juxtaposition to mean “append on the right” so, for example (u_iL_(i-1) ) means “append the current value of L_(i-1) to the current value of “
    1. u_i(σ e)=  u_i x if i=1 and e=Right_x or if i=n and e=Left_x
    2. u_i(σ e)=  u_i L_(i-1) if i>1 and

    e=Left_x

  20. u_i(σ e)=  u_i  L_(i+1)  if i<n and e=Right_x
  • The definition above causes all n components to change state in parallel when an event is appended to the event sequence of the composite system – but it’s just composition: L_i = L(u_i)=  L(u_i(σ)) and L_i(σ e)= L(u_i(σ e) ) =L(u_i(σ)e’) = e’ where e’ is calculated as above.
  • If  a device D that is constructed from components  C_1, … C_n  that are interconnected. D is a function of σ but the components don’t “see” the same events. For each component, we need a state variable u_i that is sequence valued and a function of  σ . Usually these are defined recursively: u_i(Nil)= Nil  and u_i(σe)=  concatenate(u_i,h_i(e,C_1(u_1)…  C_n(u_n ))) or something like that. That is, each event e for D causes event or events  h_i(e,C_1(u_1 )…  C_n(u_n ))  to be appended to the sequence of events u_i.
Categories
archived state maps

State equations

Download paper.
Unable to display

Categories
state maps

A mathematical basis for understanding software modularity

Download.

Categories
state maps

Practical State Machines for Computer Software and Engineering

Download paper.

[gview file=”https://www.yodaiken.com/wp-content/uploads/2016/01/practical.pdf”]

Categories
operating systems state maps

more on missed wakeup

Here are some conventions [Update: typos fix, Friday]

  • We are concerned with state machines and sequences of events. The prefixes of a sequence include the empty sequence “null” and the sequence itself.
  • Relative state: If “w” is the sequence of events that have driven a system of state machines from their initial to their current state then
    • |M is the output of state machine “M” in the current state (reached by following input sequence “w” from the initial state of M)
    • a|M is the output of M in the state reached from the current state by an “a” event.
    • z|M is the output of M in the state reached from the current state by the sequence of events “z” (if it is not clear from the context whether “z” is an event or a sequence, then we can just say which it is.)
  • Absolute state where the sequence parameter is made explicit. This is mostly useful fordefining the initial output and for when we construct composite state machines.
    • w:M is the output of state machine “M” in the state reached by following input sequence “w” from the initial state of M.
    • wa:M is the output of M in the state reached by following the sequence wa (obtained by appending event a to sequence w) from the initial state of M.
    • wz:M is the output of M n the state reached by following the sequence wz (obtained by appending event sequence z to sequence w) from the initial state of M (if it is not clear from the context whether “z” is an event or a sequence, then we can just say which it is.)
    • null:M is the output of M in its initial state.

Specific state machines

  • |Time is the current real-time.
  • |Running(p) =1 if p is executing and 0 otherwise
  • |Runnable(p) =1 if p wants to be scheduled, 0 otherwise.
  • |RequestWakeup(p,e)=1 if p is requesting a wakeup on event e, 0 otherwise
  • If |Runnable(p)=0 then a|Running(p) ≤ |Running(p) (if p is not runnable it can stop running, but not start running.)
  • If a|Runnable(p) > |Runnable(p) then there is at least one e so that a|RequestWakeup(p,e)< |RequestWakeup(p,e) (a process can only become runnable if some wakeup event happens and is cleared.)
  • If a|RequestWakeup(p,e) < |RequestWakeup(p,e) then a|Running(p)=1 (a request is only cleared if the process is actually made runnable)
  • If |RequestWake(p,e) then there is a t so that whenever z|Time ≥ |Time +t then Sum(prefixes u of z; u|Runable(p)) > 0 (if a process has requested a wakeup, it will become runnable in some bounded time – This liveness criteria is not strictly necessary)
  • Define |Safe(p) by null:Safe(p)=1 and
    • a|Safe(p)=

      • 0 if a|Running(p)=0 and a|Runnable(p)=0 and there is no e so that a|RequestWakeup(p,e) (real trouble requires that we are not runnable so can never start running unless we become runnable and cannot become runnable because we have no requests outstanding).
      • |Safe(p) otherwise (|Safe(p) does not change otherwise)
  • So what we want is to ensure that |Safe(p)=1. If a process requests a wakeup, then deschedules, and then gets a wakeup, everything is fine. The ordering is critical. If the wakeup happens before the process deschedules, but it is committed to descheduling then the process gets in trouble. If the code looks like Request e; sleep; then a wakeup event in-between the two operations is trouble. Note that Request e; if requeststill pending then sleep; is not safe unless the test and the sleep are atomic in some sense. Define |RequestOrder(p) by null:RequestOrder(p)=idle and
    • a|RequestOrder(p) =
      • requesting if |RequestOrder(p) = idle and a|RequestWakeup(p,e)>|RequestWakeup(p,e) for some e.
      • idle if a|Runnable(p) < |Runnable(p) and |RequestOrder(p)=requesting
      • error if a|Runnable(p) < |Runnable(p) and |RequestOrder(p) != requesting
      • |RequestOrder(p) otherwise.
  • |RequestOrder(p) != error does not ensure |Safe(p).
  • One solution is a lock. Suppose (Property L) If |locked(p)>0 then a|Running(p) = Running(p) and a|RequestWakeup(p,e) >= |RequestWakeup(p,e). That is, the lock prevents a running process from not running and prevents events from clearing requests -but we can make a process not-runnable while it holds the lock. Redefine RequestOrder to watch the lock.
    • a|RequestOrder(p) =
    • errror

      • if a|Locked(p) <|Locked(p) and RequestOrder(p) != (Ready or Idle)
      • or if a|Runnable(p) <|Runnable(p) and RequestOrder(p) != ready
    • locked otherwise if |RequestOrder(p) = idle and a|Locked(p) > |Locked(p) .
    • requesting otherwise if |RequestOrder(p)=locked and a|RequestWakeup(p,e)>|RequestWakeup(p,e) for some e
    • ready otherwise if a|Runnable(p) < |Runnable(p) and |RequestOrder(p)=requesting
    • idle otherwise if a|Locked(p) < |Locked(p) and |RequestOrder(p)=ready
    • |RequestOrder(p) otherwise.
  • Given Property L, |RequestOrder(p) != errror does assure |Safe(p).