cookbook:buffers

# Buffers

In this section various buffers are presented. Starting with a simple buffer, more complex bufers are presented.

## Simple buffers

An infinite buffer can be specified by a process whereby the received and sent items are stored in a list. Items are received via channel `a` and sent via channel `b`. The list is denoted by `xs`.

```proc B(chan a?,b!: item) =
|[ var xs: [item] = [], x: item
:: *( a?x; xs:= xs ++ [x]
| len(xs) > 0 -> b!hd(xs); xs:= tl(xs)
)
]|```

A finite buffer, whereby the buffer size is denoted by `N`, can be specified by:

```proc B(chan a?,b!: item, val N: nat) =
|[ var xs: [item] = [], x: item
:: *( len(xs) < N -> a?x; xs:= xs ++ [x]
| len(xs) > 0 -> b!hd(xs); xs:= tl(xs)
)
]|```

## Batch buffers

A machine in a manufacturing system can require more then one item or product before processing can start. Well-known examples of such machines are furnaces in the semiconductor industry. In that case a total of 6 items is required before processing can begin. In front of these type of machines you find batch buffers. In a batch buffer items are collected. If the number of items in the buffer is equal or more then a given batchsize `k` this batch can be sent to a process via channel `b`.

In this specification use has been made of the functions `take` and `drop`. `take(xs,k)` takes the first `k` or less items from list `xs`. `drop(xs,k)` removes the first `k` or less items from list `xs`. Note: `take([1,2,3],1) = `; `hd([1,2,3]) = 1`.

```proc B(chan a?: item, b!: [item], val k: nat) =
|[ var xs: [item] = [], x: item
:: *( a?x; xs:= xs ++ [x]
| len(xs) > 0 -> b!take(xs,k); xs:= drop(xs,k)
)
]|```

Another solution is to assume that the items to be received are lists. We have the following specification.

```proc B(chan a?, b!: [item], val k: nat) =
|[ var xs: [item] = [], ys: [item]
:: *( a?ys; xs:= xs ++ ys
| len(xs) > 0 -> b!take(xs,k); xs:= drop(xs,k)
)
]|```

## A buffered manufacturing line

As an example of a small line in the semiconductor industry, we present a buffered line with 2 etching machines processing lots in batches of 2, and 3 furnaces processing lots in batches of 6.

The objects, the items, are denoted by:

```type item  = (nat,real)
, batch = [item]```

An item consists of an identifier, a natural number and the entry time, a real number. We also introduce type `batch`. A batch is a list of items.

Generator `G` sends items to batching buffer `B`. From the buffer the items are sent to two etch processes `M`. From the etch processes the items are sent to another batch buffer and to three furnaces `M`. Finally the items are sent to exit process `E`. The exit process does some bookkeeping.

Generator `G` is:

```proc G(chan a!: batch, val ta: real) =
|[ id: nat = 1, u: -> real = expontential(ta), t: real
:: *( a![(id,time)]; t:= sample u; delay t; id:= id + 1 )
]|```

The generator sends with an exponential interarrival time an item encapsulated in a list in the system.

Batch buffer `B` is:

```proc B(chan a?, b!: batch, val k: nat) =
|[ var xs: batch = [], ys: batch
:: *( a?ys; xs:= xs ++ ys
| len(xs) > 0 -> b!take(xs,k); xs:= drop(xs,k)
)
]|```

The buffer is self explanory.

Machine `M` is:

```proc M(chan a?,b!: batch, val t0: real) =
|[ xs: batch
:: *( a?xs; delay t0; b!xs)
]|```

A machine has a processing time `t0`. The batch size in the machine is determined by the buffer in fornt of the machine.

Exit process `E` is:

```proc E(chan a?: batch) =
|[ i: nat = 0, mp: real = 0.0, phi: real
, xs: batch, x: item
:: *( a?xs
; len(xs) > 0
*> ( x:= hd(xs); xs:= tl(xs); i:= i + 1
; phi:= time - x.1
; mp:= (i - 1) / i * mp + phi / i
; !! time, "\tE\tflow time=", phi
, "\tmean flow time=", mp
, "\tthroughput=", i / time, "\n"
)
)
]|```

Model `L` is:

```model L(var ta: real) =
|[ chan a,b,c,d,e: batch
:: G(a,ta)
|| B(a,b,2)
|| M(b,c, 4.0) || M(b,c,4.0)
|| B(c,d,6)
|| M(d,e,12.0) || M(d,e,12.0) || M(d,e,12.0)
|| E(e)
]|```
cookbook/buffers.txt · Last modified: Thursday, 12 February 2009 : 09:48:54 by hvrooy

### Page Tools 