1 Requirements

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.

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, either the effect of all opertaions of { TransactionalFile.Read, TransactionalFileWrite, TransactionalFile.Seek()} within T_{i} should be visible to T_{j} or none should be visible. In the first case we would say the T_{i} precedes T_{j} and in the seconds case T_{j} preceds T_{i} and T_{i} can observe all the effects made by the operations in T_{j}.

1.2 Defenitions

Def 1- An operation is said to have ”changed” or ”affected” some data structure when it reflects the changes in the filesystem in such a way that the modification is durable and irreversible. A transaction with such an operation in its operation set is said to have changed the data

Def 2- An operation is said to have ”used” the data when it has read some data and has done some actions that is potentially irreversible. hence if the data in question was to change, op would have different resultsi. A transaction with sucj an operatins in its operations set is said to have used that data

Def 3- A transaction T_{i} is said to ”commit” at instant t_{i}, if and only if it reflects its ”changes” in the filesystem or equivalently makes it changes visible to the whole system for all members of T accesing the data at instant t_{j} such that t_{j} > t_{i} .

Def 4- For an operation a to precede operation b it means b should be able to see the effects(if any on a shared data resource) made by a.

Def 5- Succeds relationship is defined similarly.

Def 6- If operation a both precedes and succeds operation b since they do not share any resources so the changes can be made visible, a both precedes and succeds b.

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} can → T_{j}) (this defines precedes relationship for members of T)

1.3 Rules

If we denote → as the relation precedes between operations and OP_{T_{i}} as the set of all operation within T_{i} from the set {BeginTransaction, TransactionaFile.Read, TransactionalFile.Write, EndTransactioni} we would have:

Rule 1- for any pair of operations (transactions) a and b their relationship is taken from the set {→, ←, ← and →}

proof: Follows from defenition.

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

proof: Follows from the defenition of →

Rule 3- if T_{i} → T_{k} and T_{k} → T_{j} then T_{i} → T_{j}

proof: Follows from Rule 2 and Def 7.

Rule 4- If T_{j} ”commits” at instant t_{j}, and T_{commited} denotes the set of all commited transactions at t_{i} such that t_{j} > t_{i} then T_{j} should not ONLY precede any members of T_{commited} (hence they should succed)

proof: T_{i} denotes the last commited member of T_{commite}. Lets assume on the contrary T_{j} only precedes T_{i}. This means according to def 7, all operations in OP_{i} sees the effects made by those in OP_{j}.

If an operation op_{i_{1}} in OP_{i}, affects some data used by an operation op_{j_{i}} in OP_{j}, then op_{j_{1}} can not precede op_{i_{1}} since then it could not have seen the changes by it, however def 3 says it does, this is in contrats to the assumption. On the other hand, if op_{j_{1}} affects some data used by opi_{1}, then since opi_{1} has not seen the change, opj_{1} can not precede opi_{1}. If no operations in OP_{i} affects another in OP_{j}, then the set of all opeartions in OP_{i} both precede and succed those in OP_{j}, and hence the contraray to the assumption. In this case, the transaction are conceptually interchangable. In either case, T_{j} either ”succeds” or ”succeds and precedes” T_{i}. Either way it succeds the other.

The same reasoning could be done for T_{i} and T_{i−1}, T_{i−1} the last commited transaction before T_{i}. Now according to rule 3, since T_{j} succeds T_{i} and T_{i} succeds T_{i−1}, hence T_{j} succeds T_{i−1}. Same reasoning is applied for all the members of T_{commited}.

Rule 5- If T_{j} ”commits” at instant t_{j}, and T_{commited} denotes the set of all commited transactions at t_{i} such that t_{j} > t_{i} then ∀op_{i} ∈ OP_{T_{i}}, ∀op_{all} ∈ the union of OP_{j}, such that OP_{j} is the set of operations for every T_{j} ∈ T_{commited}, then op_{i} should not ONLY precede op_{all} (hence it should at least succed)

Follows immediately from rule 4 and def 7.

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

Now, if T_{i} and T_{j} do not either modify the data the other one uses, according to Rule 4 both can commit. This means even if T_{i} accesses tr_{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.

Below we will give a list of principles with the proofs on the operations and how they affect the data. We would using this table then establish the rules our system would go by. Before going to this, it should be noted that according to rule 5 even if all but one operations in a set suucced all operations in the other, still the transaction can not commit. therefore it takes only one operation to make the transaction dependent (it should succced others but can not since one of the operations in its set already preceded an operation in an already commited transaction). Formally, if there is an operation b ∈ OP_{T_{j}} and an operation a ∈ OP_{T_{j}} such that b does not succed a (or equivalently only precedes a) then T_{j} can not succed T_{i}. In the rules below T_{i} is not commited yet.

1) A seek operation in OP_{T_{i}} does not make T_{i} dependent on any data and hence does not count as ”using” (”use” as defined in Def 1).

proof: A seek operation seeks to an absolute offset within the file regradless of all operations. According to Def 2, it does not ”use” any data. Accroding to Def 5, it succeds all operations in the set of T_{committed}. Thus, according to rule 5, the seek operation within a transaction does not make the transaction unsafe to commit.

2) A read operation prior to any seek belonging to the same set of operations OP_{T_{i}} makes T r_{i} dependent on the data and offset.

proof: since according to , T r_{i} should be able to see the changes made by previously commited transactions and there is contents of the file and the starting offset that T R_{i} file has used.

3) A read operation after a seek operation both belonging to OP_{T_{i}} does not make T r_{i} dependent on the offset data but does on the contents of the file.

proof: the read operation only starts reading from the current local offset, if the offset is absolute, then it is not using any info that depends on the status of other transactions. Again Def 5 settles here for the offset (not for the contents of the file according to last principle).

4) A write operation prior to any read does not make T r_{i} dependent on any data.

proof: The write could just simply store the data in local buffer for serving read purposes, and then would actually carry on the write at commit time on the most recent commited offset. Acording to 1, T r_{i} should see thee changes and by conforming to the most recent commited offset, we acknowledge the changes made by other commited transactions

5) A write opeartion after a read makes T r_{i} dependent.

proof: follows imediately from 2 and 3 with the same dpendencies according to the prior reads.

to be continued