1 Correctness

1.1 Transactions

We have a set of Threads T each representing a transaction.The code for a Transaction is like below:

Thread.doIt(new Callable)(){ // code for transaction }

This is adopted from dstm and can and may be changed. Within this block which represents a member of set T. The functions beginTransction and endTransaction are implicitly called by the system without the intervention of the programmer.However, the programmer can read and write from TransactionalFile Objects within the blocks of a member of T. To provide consisteny the read and write from ordinary Java object files should be prohibited, otherwise the semantics of transactions would not be preserved. Hence, the sequence of operations provided to the programmer within a member of T is the set {TransactionalFile.Read(), TransactionalFile.Write()i, TransactionalFile.Seek()}. However, always a beginTransaction() and commitTransaction() (if the transaction does not abort prior to this point) are performed too.

A Transaction consists of a sequence of operations. Thus, a transaction can be represented as the {op_{1}, op_{2}, ..., op_{n}}. The flow of program should be in a manner that we could have an arbitrary serial order of the members of T (e.g. T_{5}, T_{6}, T_{1},...) or any other order. The serial order should be in such a way that for any given two members of the set T, it looks all the operations of one occur before all the operation of the other.

1.2 Defenitions

Def 1- Set of Operations: Operations are taken from the set {forcedreadoffset(filedescriptor), writeoffset(filedescriptor), readdata(inode, offset, length), writedata(inode, offset, length), commit}. We denote read operations as readoffset and readdata and write operations as writeoffset and writedata.

Def 2- Operations Sharing Resources 1- A forcedreadoffset operation and writeoffset operations are said to be sharing resources if they both operate on the same filedescriptor. 2- A readdata and writedata operations are said to be sharing resources if they both operate on the same inode AND the range of (offset, offset + length) within one overlaps with that of the other.

Def 3- A read operation can only see the writes made by write operations sharing reources.

Def 4- Commit Instant and Commit Operation: A transaction commits when it invokes the ”commit” operation. A transaction T_{i} is said to ”commit” at instant t_{i}, if and only if it reflects its ”writes” made by write operations in the filesystem or equivalently makes it writes visible to the whole system for all members of T accesing the data at instant t_{j} such that t_{j} > t_{i}. After a transaction invokes commit operation, the transactin ends and no more operation by transaction is done. An operation ∈ OP_{T_{i}} is said to commit if and only if T_{i} commits. Commit instant are not splittable, hence it appears to other transactions that all writes are refleted in the file system together.

Def 5- Precedence Relationship: If OP_{executed} = {op_{0}, op_{1}, ..., op_{n}} represnts the operations executed so far(from all transactions running), and the indices represnt the order of operations executed so far in an ascending manner, we define op_{i} → op_{j} (precedes) if and only if i < j.

Def 6- Visbility of Writes: Assume T_{i} is an uncommitted transaction and T_{commited} indicates the set of commited transaction (those which have invoked the ”commit” operation). A read operation b ∈ OP_{T_{i}} MAY ONLY see the writes(changes) made by preceding write operation a that shares resources with b AND also is subject to one of the following conditions:

1- a ∈ OP_{T_{j}} (j ≠ i) such that T_{j} ∈ T_{commited}

2- a ∈ OP_{T_{i}} and a happens before b in the natural order of the transaction. Formally, a → b

Corrolary 1- No See in The Fututre: If ∃op_{i} ∈ W RIT EOP_{T_{i}} and ∃op_{j} ∈ READOP T_{j} such that i ≠ j and op_{i} → op_{j} then if op_{j} → commit − operation_{T_{i}}, writes made by op_{j} are not seen by op_{i}.i

proof: Follows immediately from Def 5 and Def 6.

Corrolary 2- Read Must See Most Recent Comitted Write: If a ∈ OP T_{i} reads the resource r_{i} at t_{i}. In case a has multiple writer precedessors sharing r_{i} (denoted as OP_{precedessors−for−r_{i}}), then if all of them are from sets other than OP_{T_{i}}, a sees the writes made by op_{T_{j}} ∈ OP_{precedessors−for−r_{i}} such that T_{j} has the greatest ”commit instant” less than t_{i} between all transaction with such operations . Otherwise, a sees the most recent precedessor in OP_{T_{i}}.

axiom: Assume a is accessing data at t_{i}, according to Def 6, only writes by those transactions that have already committed would be visble. Hence, t_{i} is neccasarily gretaer than all members of {committime_{T_{1}}, ..., commitime_{T_{i−1}}},and hence the writes to r_{i} made by these commited transaction, have accroding to Def 4 been already reflected in the file system. Since, T_{i−1} has the greatest commit instant its changes have overriden that of previously commited transactions and thus, a reading r_{i} from file system sees these changes.

In case 2 that there are writer operations writng r_{i} and preceding a in OP_{T_{i}}, according to defenition of transaction, r_{i} should be read from the writes made by write operations in T_{i}, and as the last of such write operation overrides the written data to r_{i} by other operations, a gets to see the most recent precedessor in T_{i}.

Def 7- ∀ op_{T_{i}} ∈ OP_{T_{i}} and ∀op_{T_{j}} ∈ OP_{T_{j}} if and only if op_{T_{i}} → op_{T_{j}} then T_{i} → T_{j} (this defines precedes relationship for members of T)

Def 8- Correctness: A sequence of tarnsaction are said to be consistent if and only if a total ordeing of them according to precedence relationship can be established that demonstrates the same behavior as the execution of the program. Behavior for an operation means the data it has read. Demonstrating the same behavior thus means all the read operations should still see the same data in the new sequence as they have seen in the actual sequence.

Note 1: Def 7 and Def 8 indicate that if operations can be commuted in a given sequnce of OP_{executed} = {op_{T_{1}}(0), op_{T_{4}}(0), ...op_{T_{1}}(n)} such that a total ordering of transactions (e.g {OP_{T_{1}}, OP_{T_{2}}, ..., OP_{T_{n}})} can be obtained then the execution is consistent and correct. The eligiblity to commute is subject to conforming to Corrolary 1 & 2.

Def 9- Relocation Operations in A Sequence: In a sequence of operations OP = {op_{1}, op_{2}, ..., op_{n}}, any operation can relocate its position in the sequence unless as a result of this change, the behavior of a read operation changes (it reads different data).

Note 2: No Commute for Operations Belonging to The Same Transaction: If op_{i} ∈ OP_{T_{i}} and op_{i+1} ∈ OP_{T_{i}}, we never commute op_{i} and op_{i+1}, since even if this exchange does not change any operations behavior, there is still no point in doing this as the aim is to put all operations belonging to the same transaction together, the internal order among these is not any of our concern, and the precedence relationship among these as indicated by the execution should be maintained.

Note 3: Precedence Relationship Between Commit Operations Should Be Preserved: As a rquirement we want to have the notion that transaction are executed in the serial order imposed by their commit operations. Hence, commit operations can not be commuted.

All the rules explained later are based on the assumptions made in Note 2 & 3, hence these two types of commution are ruled out by default.

1.3 Rules

Rule 1- ∀op_{i} ∈ OP T_{i}, ∀op_{j} ∈ OP T_{j}, ∀op_{k} ∈ OP T_{k}, if op_{i} → op_{k} and op_{k} → op_{j}, then op_{i} → op_{j}

proof: Follows from the defenition of →

Rule 2- If T_{i} → T_{k} and T_{k} → T_{j} then T_{i} → T_{j}

proof: Follws from Rule 1 and Def 7.

Rule 3- Exchnaging Position of Consecutive Operations: Formally having the sequence of operations OP = {op_{1}, ..., op_{i}, op_{i+1}, ..., op_{n}}, if op_{i} ∈ OP_{T_{n}} and op_{i+1} ∈ OP T_{m} such that n ≠ m, op_{i} and op_{i+1} can exchange positions if and only if none of the follwing conditions apply:

1- If op_{i} = commit and op_{i+1} = read and op_{i+1} reads r_{k}, and ∄op_{k} in OP_{T_{m}} such that writes to r_{k}, and if there existsop_{l} ∈ OP_{T_{n}} such that writes the data r_{k}, then op_{i} and op_{i+1} can not exchange positions.

2- If op_{i+1} = commit and op_{i} = read and op_{i} reads r_{k} and ∄op_{k} in OP_{T_{n}} such that writes to r_{k}, and if there existsop_{l} ∈ OP_{T_{m}} such that writes the data r_{k}, op_{i} and op_{i+1} can not exchange positions.

proof: According to Def 9, none of the operatios in the sequence should change behavior as the result of this exchange, however in this argument only op_{i} and op_{i+1} may change behavior as those are the only operations that their postions in the sequence is changed. However, since behavior is only defined for read operations, one of these without losing generality lets say op_{i} should be a read operation on agiven resource r_{k}.

Now changing the (op_{i}, op_{i+1}) to (op_{i+1}, op_{i}) changes the behavior of op_{i} if and only if op_{i+1} writes r_{k} at the file system (all the previous precedessors are still the same, only opi + 1 has been added). This means by defenition the op_{i+1} should be a commit operation. And, if op_{i+1} is a commit operation for T_{m}, and there is at least one write operation in T_{m} writing to r_{k}, then according to Corrolary op_{i} should see the most recent results and hence if there is no precedessor for op_{i} in T_{n} itself that writes to r_{k}, then op_{i} sees the changes made by the write operarion in T_{m}. These changes could not have been seen in the first case (op_{i}, op_{i+1}) due to Corrolary 1 (No See in The Future).

Rule 4 -Relocating the Position of an Operation Within the Sequence: Given a sequence of operations OP = {op_{1}, ..., op_{i}, op_{i+1}, ..., op_{j}, op_{j+1}, ..., op_{n}}, op_{j} can be put into the standing i < j within the sequence (resulting in OP = {op_{1}, ..., op_{i}, op_{j}, op_{i+1}, ..., op_{j+1}, ..., op_{n}}) if and only if ∀op ∈ {op_{i+1}, ..., op_{j−1}}, op and op_{j} belong to different transactions and the pair (op_{j}, op) or (op, op_{j}) is not a pair subject to one of the conditions in Rule 3. The same holds true for i > j.

proof: We use induction to prove if assumptions above hold true op_{j} can be relocated to i = j − n. Assume the same OP as before. If n = 1 then since according to assumption the pair (op_{j}, op_{j−1}) is not subject to the conditions in Rule 3, these two can be easily exchanged. Now, lets assume the op_{j} can be relocated to j − n − 1, now we prove it for n. After relocation to j − n − 1, op_{i+1} immediately precedes op_{j}, as according to assumption and Rule 3 op_{j} and op_{i+1} can exchange positions. After this exchange, op_{j} has been relocated by n and to i and op_{i} now immediately precedes op_{j}.

Now we prove the other side of the argument, that if op_{j} can be relocated in i, ∀op ∈ {op_{i+1}, ..., opj − 1}, (op_{j}, op) is not a pair subject to the condition in Rule 3. Lets assume there is op in T_{i} such that (op, op_{j}) is a (readr_{n}, commit) and the commit invlolves making a write in T_{j} to r_{n} durable and a precedessor writer that writes to r_{n} does not exists for op in OP_{T_{i}} , now if op_{j} is relocated to position i, op_{j} would precede op and hence op would see the writes by the operation in T_{j} (defenition of commit Def 4 & Corrolary 2) and hence the behavior of op would change as it does not read the same data as before (the data read before could not have been the same thing due to Corrolary 1). If the pair of (op, op_{j}) is (commit, readr_{n}) the same reasoning would do.

The whole argument can be used to prove the Rule for i > j as well.

Rule 5-Operation in the Set of Execeuted Operations Belonging to Committed Transactions Should Be Able To Precede Those in The Transaction About to Commit: OP_{executed} = {op_{1}, ..., op_{n}} represents the set of executed operations before instant t_{j} and T_{committed} represents the set of committed transactions committed successfully before t_{j}. If T_{j} invokes commit operation at instant t_{j} - then T_{j} commits at instant t_{j} if and only if operations in OP can be commuted in a way such that ∀op_{i} ∈ OP_{T committed}, ∀op_{j} ∈ OP_{T_{j}}, op_{i} → op_{j}.

proof: If all those operations can be commuted tp precede those in T_{j} we could have OP_{executed} = {op_{1}, ..., OP T_{j}}. This by defenition of transaction means T_{j} can commit (it is executed in its whole entierty).

Now we have to prove T_{j} commits only if ∀T_{i} ∈ T_{committed}T_{i} → T_{j}. Now we’ll show that if all committed operations can not precede operation of T_{j} the T_{j} can not commit. OP = {op_{T_{j}}(1), ..., opT_{j}(m)} represent the operations in T_{j} excluding the commit in the order they have occured in OP_{executed}. Assume {op_{T_{j}}(k), ...opT_{j}(m)} can be relocated in OP_{executed} in the standing {n-(m-k), ...,n-1) but op_{T_{j}}(k − 1) can not. This means first of all op_{T_{j}}(k − 1) is a read operation reading r_{n}(each transaction has only one commit operation). Furthermore, this implies there is a commit operation by some transactione T_{i} between opT_{j}(k−1) and commit operation by T_{j} and ∃opinOP T_{i} such that writes r_{n} and ∄op_{i} ∈ OP T_{j} such that op_{i} → op_{T_{i}}(k − 1). On the other hand since there is a commit by T_{i} in the middle, the commit by T_{J} can not be commuted in a way so OP precedes it without any operation belonging to other transaction in the middle (two commits can not commute). Hence we can not have a sequence where all operations belonging to T_{j} are located next to each other, this contradicts the defenition of transaction, hence the transaction can not commit.

1.4 TransactionalFile Opeartions

TransactioalFiles can be either created inside or outside T. The TransactionalFile object ensures transactional access no matter where it is created and accessed. Meaning the first time T_{i} uses tf_{j} the flow of the program should look like no other piece of code (i.e Transactional and non-transactional) outside T_{i} will modify tf_{j} before OP (endtransaction)_{T_{i}}. Otherwise, T_{i} has to abort.

A Transactionalfile can be shared among any subset of the members of T. If shared, the offset is shared between these too.

2 Implications for the System

2.1 General Implications

Now, if T_{i} and T_{j} do not either write the data the other one reads, according to Rule 2 and 3 both can commit. This means even if T_{i} accesses r_{k} before T_{j} does, but T_{j} commits before T_{i}, given that T_{j} has not modified the data in use by T_{i}, T_{i} could still commit.

It should be noted that according to Rule 3 even if all but one of the transactions in the set of committed transaction precede T_{i} which is about to commit, , still the transaction can not commit. Therefore it takes only one operation to make the transaction dependent (all the committed transaction should precede this transaction but can not since one of the operations in the committed transaction does not precede an operation in this transaction). Formally, if there is an operation b ∈ OP_{T_{j}} and an operation a ∈ OP_{T_{i}} such that a does not precede b then T_{i} can not precede T_{j}. In the rules below T_{i} is not commited yet and T denotes the set of all commited or active transactions.