Model specification

Copyright © 2011 Gabriel Zs. K. Horvath

This is my first attempt at giving a more formal definition of my software transactions model. Undoubtedly, a post which will be frequently updated.

Consider a system composed of the following:

• A single transaction manager holding a unique global version number
• Transactions
• Threads
• Semi-mutable versioned variables managed by the transaction manager
• Non-versioned transaction-local immutable variables
• External resources, these can be either read from or written to
• A garbage collector

The program consists in the execution of transactions in one or more concurrent threads.

The transaction manager is responsible for the creation, duplication, cancellation and closure of transactions. It also manages the merging and joining of transactions as well as the creation of contiguous and notification transactions and the registration of notification subscribers. A new transaction is denoted by T_N where N is the value of the global version number when the transaction is created. A transaction commits by adding to each of the modified versioned variables a new version labeled with the unique version number M+1 where M is the global version number when the transaction commits. The transaction manager ensures that every commit operation uses a distinct and monotonously increasing version number.

The garbage collector is responsible for the disposal of unreachable data across the entirety of the system.

In terms of threading, there is a one-to-one mapping between threads and transactions. Every thread always has one associated transaction, every transaction is executed in one and only one thread. A thread spawned in the context of transaction A is executed in the context of a transaction duplicated from its parent thread’s transaction.

Local variables are not visible outside the transaction they are declaring in. Their lifetime matches the transaction’s lifetime. Newly created local variables are only visible in the thread they are created in and their subsequently spawned child threads.

A transaction consists of a sequence of operations on semi-mutable versioned variables, local variables and external resources. These operations can be executed in any number of concurrent threads. A transaction, denoted by T_N, is labeled with a version number N which matches the global version number at the time the transaction started. The following operations are supported:

• Creating and initializing a new local variable
  
• Reading from a local variable
  
• Reading from a semi-mutable versioned variable: a read operation o with arguments x on a semi-mutable versioned variable v in the context of transaction T_N is denoted by R_v,o,N(x). All read operations are stored on a per transaction basis. A read operation always returns data which has been committed. Hence semi-mutable variables are immutable for the duration of the transaction. Semi-mutable versioned variables also support unchecked reads which are not recorded, hence not validated.
  
• Writing to a transactional box: a write operation o with arguments x on a transactional box v in the context of transaction T_N is denoted by W_v,o,N(x). All write operations are stored on a per transaction basis in the order they are invoked. The writes are stored but remain un-committed and hence unobservable until the transaction commits. Writes trigger the validation of read operations.
• Read operations from external resources
  • Checked read: a checked read operation on external resource r is denoted by r_r,N(x). All checked reads are stored on a per transaction basis.
  • Unchecked read are not recorded.
• Write operations to external resources
  • Checked write: a checked write operation on external resource r is denoted by w_r,N(x). Write operations are not performed during the execution of the transaction but are recorded on a per transaction basis in the order they were invoked in. Checked external writes trigger the validation of read operations.
  • Unchecked write: an unchecked write operation on external resource r is denoted by W_r(x). Write operations are not performed during the execution of the transaction but are recorded on a per transaction basis in the order they were invoked. Unchecked external writes do not trigger the validation of read operations.

The state of all versioned variables for a given version number N defines the state of the system for that version number is denoted by S_N.

A versioned variable which is either written to or read from during a transaction is said to be enrolled in the transaction. A versioned variable can be enrolled in multiple transactions concurrently.

A semi-mutable versioned variable which has been written to can only ever enter the closing state of one transaction at a time. A semi-mutable versioned variable can concurrently enter the closing stage of all the transactions in which it has only been read. At the time at which a transaction T_N enters its closing stage, the global version number of the system is denoted by M ³ N. The previous requirement ensures that no new version can be committed to the enrolled variables during the closing stage.

The validation stage consists in ensuring the following:

• all reads performed on the semi-mutable versioned variables during the transaction against version N return the same value at the validation stage when performed against version M:

R_v,o,N(x) = R_v,o,M(x)

• all checked reads performed on external resources during the transaction return the same value when executed at commit time:

r_r,N(x) = r_r,M(x)

This is equivalent to re-executing all the reads performed during the transaction at the validation stage. If all reads return the same value, all input to the atomic block is guaranteed to be the same; this is then equivalent to re-executing the transaction at commit time. We make the implicit assumption that unchecked external reads return the same value if they were to be re-executed at this validation stage.

The validation stage is only ever carried out if there are write operations to be performed on semi-mutable versioned variable or normal write operations on external resources. Unchecked write operations on external resources do not trigger validation.

If the validation is successful the transaction enters its commit phase. The recorded writes W_v,o,N(x) are performed against the version M of the semi-mutable versioned variables resulting in a new version P+1, where P ³ M+1 is the value of the global version number when the transaction commits. The external writes w_r,N(x) are also executed. All the variables enrolled in the transaction must have their new version created before the global version number gets updated to P+1. This ensures that the new versions appear to be created atomically.

A contiguous transaction is one which is guaranteed to see the system in the state its parent transaction put it in. A notification transaction is a contiguous transaction which contains the write operations which were committed by its parent transaction.

Transactions can be either merged or integrated together.

A transaction A is integrated into transaction B by appending the write operations from B to the write operations in A, resulting in a last-write-wins policy for the write operations from B. The reads from B are added to A so that they will be independently validated when transaction A closes.

Transactions A and B are merged by combining the writes from both transactions. This is only permitted if all the writes from both transactions commute, thus excluding any last-write-wins situation. The reads from both transactions are merged together so that at commit time the reads from both A and B transactions are validated.