--- /dev/null
+\documentclass[a4paper, 11pt]{article}
+\begin{document}
+\section{Requirements}
+\subsection{Transactions}
+We have a set of Threads $T$ each representing a transaction.The code for a
+Transaction is like below:
+
+\hspace{12mm} Thread.doIt(new Callable)()\{
+
+\hspace{12mm} // code for transaction
+
+\hspace{12mm} \}
+
+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$. \\
+
+\subsection{Defenitions}
+
+Def 1- 1-An operation in $T_i$ is said to have "changed" or "affected" some data structure in correspondece to all members of $OP_{T- T_i}$ , 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 $T_i$ in its operation set is said to have changed the data 2- An operation in $T_i$ is said to have "changed or affeced the data in correspondence to all the operations in $OP_{T_i}$ as soon as the operation is encountered \\
+
+Def 2- An operation in $T_i$ 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 results. A transaction with such an operation in its operations set is said to have used that data. Any data read and used within a transaction at its commit instant does not count as using. "Use" can just be attributed to the operations actually reading data before commit instant. \\
+
+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$ . An operation $\in 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 changes are refleted in the file system together.\\
+
+Def 4- $\forall op_i \in OP_{T_i}$, $\forall op_j in OP{T_i}$, $op_i$ precedes $op_j$ if and only if $op_j$ does not use the data changed by $op_i$ OR if it does, then $op_j$ should be able to see the changes made by $op_i$ unless data has been changed by a more recent precedessor \\
+
+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- $\forall$ $op_{T_i}$ $\in OP_{T_i}$ and $\forall op_{T_j}\in OP_{T_j}$ if and only if $op_{T_i} \rightarrow op_{T_j}$, then $T_i$ \emph {can} $\rightarrow T_j$) \hspace{8mm} (this defines precedes relationship for members of $T$) \\
+
+Def 8- An operation $op \in OP_{T_i}$ should be able to see the "changes" 1- made by $OP_{T_commited}$ and 2-$oper \in OP_{T_i}$ that in natural order of transaction occur before $op$
+
+\subsection{Rules}
+If we denote $\rightarrow$ 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 \{$\rightarrow$, $\leftarrow$, $\leftarrow$ and $\rightarrow$\} \\
+
+proof: Follows from defenition. \\
+
+Rule 2) If an operation $a \in OP{T_i}$ has multiple prcedecors (denoted as $OP_{precedesors}$) that their changes overlap each other, then if all of them are from sets other than $OP{T_i}$, $a$ sees the "changes" made by the $op_i \in OP_{predecesors}$ such that $op_i$ has the greatest "commit instant" . Otherwise, $a$ sees the most recent precedesor in $OP{T_i}$. \\
+
+proof: the first part follows from Def 4 , second derives from Def 4 and second part of Def 1.\\
+
+Rule 3- $\forall op_i \in OP{T_i}$, $\forall op_j \in OP{T_j}$, $\forall op_k \in op{T_k}$ if $op_i \rightarrow op_k$ and $op_k \rightarrow op_j$ then $op_i \rightarrow op_j$ \\
+
+proof: Follows from the defenition of $\rightarrow$ \\
+
+
+Rule 4- if $T_i \rightarrow T_k$ and $T_k \rightarrow T_j$ then $T_i \rightarrow T_j$ \\
+
+proof: Follows from Rule 2 and Def 7. \\
+
+
+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 $T_j$ should not \emph ONLY precede any members of $T_{commited}$ (hence they should succed)\\
+
+proof: $T_i$ denotes the last commited member of $T_{commited}$. 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 $op{i_1}$, then since $op{i_1}$ has not seen the change, $op{j_1}$ can not precede $op{i_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 6- 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 $\forall op_i \in OP_{T_i}$, $\forall op_{all} \in$ the union of $OP_j$, such that $OP_j$ is the set of operations for every $T_j \in T_{commited}$, then $op_i$ should not \emph ONLY precede $op_{all}$ (hence it should at least succed)\\
+
+Follows immediately from rule 4 and def 7.
+
+\subsection{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$ \emph {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 \emph {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.
+
+\section{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 6 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 \in OP_{T_j}$ and an operation $a \in 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 and $T$ denotes the set of all commited or active transactions. \\
+
+Assumption : The reads within transaction do actually occur when they are encountered. However, no change to the file system is done before commit instant as said before (writes, changing the offset and etc.)\\
+
+
+Assumption: seek operation means after this operation is executed, the offset should be at the chosen value regardless of the actual value of the offset in the file system.
+
+
+Principle 1) If an operation $a$ that "uses" some data (reads the data at some $t < t_{commit}$(the commit instant)), it should be ensured that the data is still valid in the actual file system at $t_{commit}$ (commit instant) or $T_i$ has to abort.//
+
+proof: If the data is not valid anymore it means the data has changed since $t_{i-1}$. This implies at least one operation $b$ has chaged the data since the use. $b$ is either a succesor in the same transaction or a different one. According to Def 1 and Def 3, however if $b$ is in the same transaction, then $b$ can not have commited yet and hence the changes are not reflected in the filesystem. Hence $b$ belongs to a different transaction namely $T_j$. Since $T_j$ should have already commited, according to Rule 6 all operation in $OP_{T_i}$ should succed those in $OP_{T_j}$, however, we know there is at least an operation $a$ that does not succced $b$ (since it has not seen the "changes" made by $b$). Hence, $T_i$ can not commit.\\
+
+
+Principle 2) 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).\\
+
+The seek operations seeks to an offste within the file descriptor regardless of the changes made by opretaions in all transaction, hence the result would always be the same so according to Def 2 it does not count as using.\\
+
+Principle 3) 1- A read operation in $OP_{T_i}$ "uses" contents read and makes $T_i$ dependent on the file contents read.\\
+
+proof: Due to assumtion 1 and since the data read by this operation can be used for computation, in case the data read would change, the data and hence computations results would be different. According to Def 2 it uses the data\\
+
+Principle 4) 1- A write operation in $OP_{T_i}$ does not make $T_i$ dependent on file contents.\\
+
+proof: The result of a write would always be the same contents thus, according to Def 2 does not count as using.\\
+
+Assumption: Each operation has an offset status assioated with it. We call this operation.offsetstatus\\
+
+Assumption: An operation with Speculative offset means the offset that the operation would be perfomed at can be relocated in the commit instant. An operation with absolute offset means the value is absolute and does not depend on any other operation OR the operation only specifies a specific value for the offset for the next operation (i.e. seek). An operation with defenite offset means the offset value that operation has to be carried on from, can not be relocated, but still could have changed before commit instant by other committed transactions. \\
+
+Principle 5: an operation with defeinte offset status assosiated with it is the only one "using" the offset value.\\
+
+proof: For speculative and absolute it comes form the defeniton that they do not count as using, since one is determined at commit instant and hence read at the same time, and the other is always the same value. However, with defenite, if some other transaction changes the offset of the file descriptor, then the result of the operation would have been possibly different. According to Def 2 it uses the offset data.\\
+
+
+
+
+Def: We define a function $f$ that takes as input an operation (i.e. seek, read, write) and gives as the output the offsetstatus assosiated with that operation. In speaking, $f$ determines the offsetstatus assoiated with an operation given that it is the ONLY operation in the operation set of the transaction. \\
+
+1- $f$(Seek) = Absolute
+
+proof: seek operation does not invlove reading offset value hence, according to assumptions it is considered as absoulute.\\
+
+2-$f$(Read) = Defenite
+
+proof: Since according to Principle 3, read is actually done before the commit instant and hence can not be relocated in the commit instant. According to Principle 1 and 5 the offset the read is done from should not be affected by other members of $T$ before this transaction gets to its commit instant. This means not the only offset can not be relocated, but a check should be done at the commit instant for its validity.\\
+
+3-$f$(Write) = Speculative
+
+proof: If write is the only operation, then since according to Principle 4 the write does not use any file contents before commit instant, hence the ofsset value can be determined at commit instant from the most recently commited offset value by then. Then the write is done on the offset. This preserves the semantics since the commit instant is atomic by defenition and Rule 6 and 5 are preserved, as the write operation is getting the most recent data(offset) and hence would see all the changes made to it by commited transactions so far and hence this write operation would succed all the operations in other commited transaction. Consequently this transaction can succed those.\\
+
+Requirements: To determine an operation should use Absolute, Define or Speculative offset type (the first and third would be used in commit instant) respective to other operatins in the set, the requirements below should be provided:\\
+
+Req 1- 1-Any operation follwoing an operation $op$ (which belongs to the same set of operations) with offsetstatus = Absolute, has offsetstatus = Absolute itself. 2-Any operation that applying $f$ to it would yield in Absolute, has offsettype = absolute \\
+
+proof: 1-Lets assume $op$ is the first operation with offsettype = Absolute in the set of operatopns. The immediate operation ($op_{imm}$) after $op$ uses the absolute offset specified by $op$ or the absolute offset advanced by a certain number in case of read or write. $op_{imm}$ either advances this value or specifies another absolute value, in either case the offset type for $op_{imm}$ would be absolute. The same reasoning could be done for all the follwing operations.\\
+
+2- Since such an operation is seek and seek regardless of all other operation (in and out of transaction) sets the offset and hence is always absolute.\\
+
+Req 2- 1- Any operations $op$ that applying $f$ on it would yield in Definite, has offsettype = Defenite unless speified otherwise by Req 1 2-Any operation immediately follwoing an operation $op$ (which belongs to the same set of operations) with offsetstatus = Defenite, has offsetstatus = Defenite itself. unless specified otherwise by Req 1\\
+
+proof: 1- if $f$ makes the output Defenite it means this operation should "use" offset value at that time unless some previous instruction has set the offset to specific value independent of other transactions and thus changing the offset value would not have any effect on the outcome of $op$ as the value $op$ should be carried on from would be independent. Operation having such an effect is the one with Absolute offsettype.\\
+
+2- The following operation should be Defenite type since $op$ has bound the offset to a value that should be validated at commit instant (Principle 1), unless it is a seek that only sets the offset.
+
+Req 3: Any operation with offsetstaus = Defenite, should change the offsetstatus for prveious operations with a value of Speculative, to Defenite.\\
+
+If $op.offsettype = Definte$ means no previous operations are Absolute (Req 1). So it just could be a mixture of Speculative and Defenite. Lets assume $op_{Def}$ as the first operation after a $op_{spec}$ a Speculative one (Rq 2 ensure after A Defenite there is no Speculative). $op_{Def}$ makes the offset bound to a specific value and $op_{Def} succeds $op{Spec}$ so it should be able to see the changes made by $op{Spec} this neccesitaes that $op{Spec}$ be done at a specific offset such that when advanced as the effect of operation, it gives the offset chosen by $op{Def}$, otherwise $op{Def}$ does not see the effects of $op{Spec}$ which is in contradiction to presumtions. Hence, $op_{Spec}.offsettype$ should be converted to Defenite.\\
+
+Req 4: Any operation $op$ which applying $f$ on it yields in Speculative has offsettype=Speculative unless specified otherwise by previous requirements.\\
+
+proof: If we denote $OP_{prev}.offsettype$ as the offsettypes for the prviously encountered operations, considering all requirements this means all (if any) the members of $OP_{prev}$ should be Speculative for $op$ to be able to be Speculative. In this case the offset passed to $op$ is Speculative and if $op$ is Speculative as considered alone then it would carry on the actions in the passed-in Speculative offset.\\
+
+
+Def: We define a function $g(offsetstat_1, offsettat_2, ..., offsetstat_{n-1}, operation)$ that takes an input $n-1$ number of $op.offsetstatus$ plus an operation and gives as the output $n$ number of $op.offsetstatus$. The $g$ functions provides the requirements mentioned above. Follwing rules determine the output, the rules are ordererd according to their priority:\\
+
+1- if $f(operation) = Absolute$, $g(offsetstat_1, ..., {offsetstat_{n-1}}, operation) = ({offsetstat_1}, ..., {offsetstat_{n-1}}, Absolute)$ leaving all offsetstats intact.\\
+
+2- if $f(operation) = Defenite$:\\
+
+\hspace{ 8mm}
+ 2.1- if $\exists offset \in \{offsetstat_1, ..., offsetstat_{n-1}$\} such that offset = Absolute, $g(offsetstat_1, ..., offsetstat_{n-1}, operation) = (offsetstat_1, ... ,Absolute)$ leaving all offsestats intact.\\
+
+\hspace{ 8mm}
+ 2.2- else $\forall offsetstat \in (offsetstat_0, ..., offsetstat_{n-1})$ if offsetstat = Speculative, change its value to Defenite in the output of $g$, plus appending a Defenite to the output (for instane $g(speculative, speculative, read) = (defenite, defeinte, definte)$)\\
+
+3- if $f(operation) = Speculative$:\\
+
+\hspace{ 8mm}
+ 3.1- if $\exists offset \in \{offsetstat_1, ..., offsetstat_{n-1}\}$ such that offset = Absolute, $g(offsetstat_1, ... offsetstat_{n-1}, operation) = (offsetstat_1, ... Absolute)$ leaving all offsestats intact.\\
+
+\hspace{ 8mm}
+ 3.2- else if $\exists offsetstat \in \{offsetstat_1, ..., offsetstat_{n-1}\}$ such that offsetstat = {Defenite}, $g(offsetstat_1, ..., offsetstat_{n-1}, operation) = (offsetstat_1 ,..., offsetstat_{n-1}, Defenite)$\\
+
+\hspace{ 8mm}
+ 3.3- else $g(offsetstat_1, ..., offsetstat_{n-1}, operation) = (offsetstat_1, ..., offsetstat_{n-1}, Speculative)$\\
+
+
+1, 2.1, 3.1 ensure Req 1. 2.2 and 3.2 ensures Req 2. 2. ensure Req 3, and finally 3.3 provides Req 4.
+
+
+
+
+
+
+
+
+%$f: \{op_0.offsetstatus,op_1.offsetstatus,...,op_{n-1}.offsetstatus\} \rightarrow \{op_0.offsetstatus, op_1.offsettatus,...,op_{n-1}.offsetstatus,op_m.offsetstatus, \}
+
+
+
+%2- Since due to assumption 1, the read should be actually done, it has to be done from a real offset, and since the commited offset at the commit instant is unknown in adavance, the currenlty most recent commited offset is chosen. This makes the read and hence transaction dependent on the offset value read.
+
+%2- Since all the following read and writes at least succed this seek operation, they should be able to see the changes made by it unless some other operation in between changes the data in question (offset). Lets first assume the operation ($op$) following the seek. If $op$ is a read or write, then it would carry on reading or writing the data from the absolute offset so it would advance the aboslute offset resulting in another absolute offset and hence no "use" of the actual offset would be applicable. If the following is a seek, then the resultant offset would be another absolute offste. Same reasoning could be done for all the succeding operations and hence the offset would be still absolute. To prove only seek can make the offset absolute it should have been made absolute by read or write, however as we'll see in Principles 2 and 3 they can not yield in an absolute offset. Hence, an absolute offset indicates there has been a seek.\\
+%According to priciple 1 the offset chosen should be validated at the the commit instant.\\
+\section{Implementation Overview}
+
+%proof: A write operation writes to the most recently commited offset (unless imposed otherwise by a seek or a prior read or a following read as shown above) of the file descriptor. According to Def 2, it does not "use" any data. Since the write does not happen till commit instant, the offset chosen during the execution of transaction can be speculative, and the actual offset to be written to, is determined at the sommit instant, when the most recently commited offset is known.
+Now we will describe the components of our system and demosntrate how the algorithm
+
+
+
+
+
+
+
+
+
+to be continued
+
+%\begin{tabular}{c|c|c|}
+\end{document}
projects / IRC.git / commitdiff