User Tools

Site Tools


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) = [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"
           )
    )
]|

The buffered manufacturing line

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