source: CIVL/examples/concurrency/bank.cvl@ 8d704f9e

/* bank.cil

simple exercise in multitasking verification using CIVL. 

*/

/* ======================================================================== 
   constants
 */
#define NUM_ACCOUNTS 3

#define true 1
#define false 0


/* ======================================================================== 
   prototypes
 */
void init();
int withdraw( int account_num, int amount );
int deposit( int account_num, int amount );
int balance( int account_num );
int transfer( int to_account_num, int from_account_num, int amount );
void lock_account( int account_num );
void unlock_account( int account_num );

/* ======================================================================== 
   global variables
 */
int account_balance[ NUM_ACCOUNTS ];
int account_locked[ NUM_ACCOUNTS ];

/* ======================================================================== */

void lock_account( int account_num )
/* TODO: Why does this function have to appear before code where it is called,
        even though it has a prototype, above?  
*/
{{
   $assume 0 <= account_num;
   $assume account_num <= NUM_ACCOUNTS;

   // this needs to happen atomically -- does it?
   $when (account_locked[account_num] == false) account_locked[account_num]= true;
}}

/* ======================================================================== */
void unlock_account( int account_num )
/* TODO: Why does this function have to appear before code where it is called,
        even though it has a prototype, above?  
*/
{{
   $assume 0 <= account_num;
   $assume account_num <= NUM_ACCOUNTS;

   account_locked[ account_num ]= false;
}}

/* ======================================================================== */
void init ()
{{
   int acct_num;
   for ( acct_num= 0; acct_num < NUM_ACCOUNTS; acct_num++ )  {
      account_balance[acct_num]= 0;
      account_locked[acct_num]= false;
   }
}}

/* ======================================================================== */
int withdraw( int account_num, int amount )
/* Return value: false if success, true if an error occurred 
 */
{{
   $assume 0 <= account_num;
   $assume account_num <= NUM_ACCOUNTS;
   $assume amount >= 0;

   int result;
   
   // begin transaction
   lock_account( account_num );

   if ( account_balance[account_num] >= amount )  {
      account_balance[account_num]= account_balance[account_num]- amount;
      result= false;
   } else {
      result= true;
   }

   // end transaction
   unlock_account( account_num );

   return result;
}}

/* ======================================================================== */
int deposit( int account_num, int amount )
/* Return value: false if success, true if an error occurred 
 */
{{
   $assume 0 <= account_num;
   $assume account_num <= NUM_ACCOUNTS;
   $assume amount >= 0;

   // begin transaction 
   lock_account( account_num );

   account_balance[account_num]= account_balance[account_num]+ amount;

   // end transaction
   unlock_account( account_num );

   return false;
}}

/* ======================================================================== */
int balance( int account_num )
/* Return value: the balance of the indicated account
 */
{{
   $assume 0 <= account_num;
   $assume account_num <= NUM_ACCOUNTS;

   int balance= 0;

   // begin transaction
   lock_account( account_num );

   balance= account_balance[account_num];

   // end transaction
   unlock_account( account_num );

   return account_balance[account_num];
}}

/* ======================================================================== */
int transfer( int to_account_num, int from_account_num, int amount )
/* Return value: false if success, true if an error occurred 
 */
{{
   $assume 0 <= to_account_num;
   $assume to_account_num <= NUM_ACCOUNTS;
   $assume 0 <= from_account_num;
   $assume from_account_num <= NUM_ACCOUNTS;
   $assume from_account_num != to_account_num;
   $assume amount >= 0;

   int result= false;

   // begin transaction
   if ( from_account_num < to_account_num )  {
      lock_account( from_account_num );
      lock_account( to_account_num );
   } else {
      lock_account( to_account_num );
      lock_account( from_account_num );
   }

   if ( account_balance[from_account_num] >= amount )  {
      account_balance[from_account_num]-= amount;
      account_balance[to_account_num]+= amount;
      result= false;
   } else {
      result= true;
   }

   // end transaction
   if ( from_account_num < to_account_num )  {
      lock_account( to_account_num );
      lock_account( from_account_num );
   } else {
      lock_account( from_account_num );
      lock_account( to_account_num );
   }

   return result;
}}

/* ======================================================================== */
/* main() and its helper ftns
 */
void main_a()
{{
   withdraw( 0, 50 );
   transfer( 0, 1, 50 );
   deposit( 2, 100 );
}}

void main_b()
{{
   deposit( 1, 10 );
   withdraw( 2, 50 );
   transfer( 2, 0, 20 );
}}

void main() 
{{
   int acct_num= 0;

   //;;$proc proc_a;
   //;;$proc proc_b;

   init();

   /* give all accounts some money */
   for ( acct_num= 0; acct_num < NUM_ACCOUNTS; acct_num++ )  {
      deposit( acct_num, 100 );
   }

   //;;proc_a= $spawn main_a();
   //;;proc_b= $spawn main_b();

   //;;$wait proc_a;
   //;;$wait proc_b;
   // TODO: resolve why this temporary code generates an error.
   main_a();
   main_b();
}}

/* ======================================================================== */
/* end of file */