Transactions

A proposal for transaction based concurrency in Eiffel by Colin LeMahieu,

Rationale: The intractability of determining if a program based on locks will deadlock in general necessitates using alternative forms of concurrency.

Abstract: The Eiffel language already supports the basic idea of transactions in features. A feature either completes in its entirety or an exception is raised. The only shortfall of the current implementation is that any side effects made before the feature completes are not aborted in the transactional sense. If we adapt the semantics of a feature to include the idea of a transactional feature, we will be able to implement concurrency through transactions in the Eiffel language cleanly.

Behavior:

• A feature can be a transaction
• Transactional features guarantee atomicity and isolation across the execution of the feature
• When a transactional feature calls another transactional feature, the transactions are composed.
• When a transactional feature is aborted it is automatically retried until it is not aborted.
• External features without abort and commit semantics are executed when all transactions have been committed or aborted and executed serially with respect to the system, this is ensured by the runtime.

Syntax: Use the 'transaction' keyword to define a feature as a transaction

feature
 
  obligatory_transfer_example(account, amount) is
    transaction
      withdraw(account, amount)
      deposit(account, amount)
    end
 
  withdraw(account, amount: INTEGER) is
    transaction
      account.balance.withdraw(amount)
    end
 
  deposit(account, amount: INTEGER) is
    transaction
      account.balance.deposit(amount)
    end

Use the 'external', 'abort', and 'commit' keywords to define a transactional external feature. 'External' defines the external transaction functionality. 'Abort' defines functionality to roll back any state changed in 'external'. 'commit' defines functionality to commit the transaction of 'external'.

feature
 
  external_feat is
    external
      ""
    abort
      ""
    commit
      ""
    end

Design by contract:

• Preconditions and postconditions retain ECMA semantics.
• Example: If a transactional feature 'f' wants to call feature 'g' with a precondition 'a', 'f' can check 'a' before calling 'g' and is assured that 'a' will be the same once 'g' is being executed by the transactional nature of 'f'; 'a' will either remain valid or 'f' will be aborted and retried.
• Precondition wait semantics as introduced with SCOOP do not need to be used.
• Class invariants determine the consistency of transactions and are checked every time a transaction is committed and after it is aborted

Deferred features:

• Deferred features can be redefined to be either a transaction or not. As long as the feature satisfies its contract, the detail of whether the called feature is implemented as a transaction doesn't matter.

Agents:

• Agent semantics will not change.

Mutexes:

• Code using mutexes will continue to work, however they should be replaced with transactional code as soon as possible to avoid the possibility of deadlocks associated with locking.

Notes:

• Unlike database transactions, durability is not guaranteed with feature transactions, memory is inherently volatile in the face of system errors.

• It's impossible for a transactional feature to reliably act on a legacy external feature. During the execution of a transactional feature, any of the actions may be aborted and retried and since legacy external features cannot be aborted, there is no reliable way to undo that action.

• It might be better to use a keyword to define a feature as non-transactional instead of using a keyword to define a feature as transactional.

Examples

Transactions are assured with transactional memory, probably implemented as software transactional memory.

Example of transaction:

feature
 
  correct_removal(container: DISPENSER) is
    transaction
        -- This is a transaction so it is assured to be atomic and isolated
      if
        not(container.is_empty)
      then
        container.remove
      end
    end

This feature is assured to be correct because is is isolated and atomic with respect to the system. If the container has been modified between the call to is_empty and remove, the feature would be aborted and retried.

feature
 
  incorrect_removal(container: DISPENSER) is
    do
      if
        not(container.is_empty)
      then
        container.remove
      end
    end

This is the standard example of concurrency issues with preconditions. The container can change between the call to is_empty and remove. Using transactions avoids this.

Legacy externals example

feature
 
  use_legacy_external(item: LEGACY_ITEM) is
    do
      print_item(item)
      log_item(item)
      -- At this point the runtime will block until print_item and 
      -- log_item have both committed, it will ensure nothing is running 
      -- in the system and then run the external item serially.  
      -- This is the non-concurrent way to ensure something executes as 
      -- a transaction, isolated and atomic.
      use_item(item)
    end
 
  use_item(item: LEGACY_ITEM) is
    external
      "..."
    end
 
  print_item(item: LEGACY_ITEM) is
    do
      ...
    end
 
  log_item(item: LEGACY_ITEM) is
    do
      ...
    end

Example of need for runtime checks on agents in systems that allow legacy external features.

class A
feature
  other: B
  legacy_external_feature is
    external
      "..."
    end
 
  call_transaction_with_agent is
    --This feature would compile since it would be undecidible if 'other' is attached to an instance of C at runtime
    do
      other.redefined_call(agent legacy_external_feature)
    end
 
  a_transaction is
    --This feature is a compile time error as a validity constraint
    transaction
      legacy_external_feature
    end
 
end
 
deferred class B
feature
  redefined_call(the_agent: PROCEDURE[TUPLE[]]) is
    --A reason to allow deferred features to be redefined
    --to a transaction or not is for syntax simplicity
    --and because the only time it matters is when building
    --new transactions on top of legacy code
    deferred
    end
end
 
class C
inherit B
feature
  redefined_call(the_agent: PROCEDURE[TUPLE[]]) is
    transaction
      io.put_string("Line 1")
 
      --This call is a runtime exception.  The probability of this happening
      --is low because people building transactional code should be looking
      --at replacing legacy external features with transactional externals
      --or some other transaction abstraction over externals
      the_agent.call
 
      io.put_string("Line 2")