Path: utzoo!utgpu!news-server.csri.toronto.edu!bonnie.concordia.ca!uunet!munnari.oz.au!metro!ipso!runxtsa!chrisv
From: chrisv@runx.oz.au (Chris Velevitch)
Newsgroups: comp.lang.eiffel
Subject: Re: Functions without side effects (was Old confusion)
Message-ID: <1991Jun4.041233.19046@runx.oz.au>
Date: 4 Jun 91 04:12:33 GMT
References: <1991May30.141218.3446@mstr.hgc.edu> <327@alfrat.uucp>
Organization: RUNX Un*x Timeshare.  Sydney, Australia.
Lines: 88

In article <327@alfrat.uucp> roy@alfrat.UUCP (Roy Phillips) writes:
>  As a second case for functions with side effects, consider the interface of
>  a mutual exclusion class, loosely based upon Djistra's P&V algorithm:
>  
>  --
>  -- MONITOR  --  Resource Allocation Monitor providing mutual
>  --              exclusion facilities
>  --
>  -- %Z%%Y%:%M%   %I%
>  
>  indexing
>  
>     date: "$Date: %D% %T% $";
>     revision: "$Revision: %R%.%L% $";
>  
>     authors: roy;
>     names: monitor;
>     access: exclusive;
>  
>  deferred class MONITOR export
>  
>     free,
>     test_and_set,
>     request,
>     release,
>     got_resource
>  
>  feature
>  
>     free: BOOLEAN is
>        -- is the resource we are managing available?
>     deferred
>     end; -- free
>  
>     test_and_set: BOOLEAN is
>        -- is the resource we are managing available to us?
>     deferred
>     ensure
>        Result = True implies got_resource;
>        Result = False implies not free and not got_resource
>     end; -- test_and_set
>  
>     request: BOOLEAN is
>        -- return True when we have control of the resource
>     require
>        -- not free implies "wait until resource free"
>     deferred
>     ensure
>        got_resource
>     end; -- request
>  
>     release is
>        -- make resource available again
>     require
>        free = False and then got_resource
>     deferred
>     ensure
>        not got_resource
>     end; -- release
>  
>     got_resource: BOOLEAN
>        -- return True if we have successfully obtained 
>        -- exclusive accesss to resource
>     deferred
>     ensure
>        Result = True implies not free
>     end; -- got_resource
>  
>  end -- class MONITOR
>  
>  Seperate `request' and `release' operations are an obvious
>  requirement (implemented as a function and a procedure respectively)
>  but it is essential to provide a `test_and_set' routine, that returns
>  a boolean `success/fail' status and grabs the resource if it is free
>  - hysteresis between calling `free' and `request' could cause the application
>  to perform an undesired wait inside of `request'.

Testing the result of 'test_and_set' routine is the same as testing
'got_resource'. So 'test_and_set' should be a procedure and the result
available through some other feature, in this case 'got_resource'.


Chris
-- 
--
Chris Velevitch, Voice: +61 2 906 6100, Fax: +61 2 906 6069
Cee Data Systems, 22/39 Herbert St, St Leonards NSW 2065, Australia
Internet: chrisv@runxtsa.runx.oz.au, UUCP: uunet!runxtsa.runx.oz.au!chrisv