1 \documentclass[a4paper, 11pt]{article}
4 \subsection{Transactions}
5 We have a set of Threads $T$ each representing a transaction.The code for a
6 Transaction is like below:
8 \hspace{12mm} Thread.doIt(new Callable)()\{
10 \hspace{12mm} // code for transaction
14 This is adopted from dstm and can and may be changed. Within this block which
15 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. \\
17 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. 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$. \\
19 \subsection{Defenitions}
21 Def 1- \emph{Set of Operations}: Operations are taken from the set \{readoffset(fildescriptor), writeoffset(filedescriptor), readdata(inode, offset, length), writedata(inode, offset, length)\}. We denote read operations as readoffset and readdata and write operations as writeoffset and writedata.\\
23 %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 \\
25 Def 2- \emph{Operations Sharing Resources} 1- A readoffset 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.\\
27 Def 3- A read operation can only see the writes made by write operations sharing reources.\\
29 Def 4- \emph{Commit Instant}: A transaction $T_i$ is said to "commit" at instant $t_i$, if and only if it reflects its "writes" mabe 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$ . 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 writes are refleted in the file system together.\\
31 Def 5- \emph{No See In Future}: Assume $T_i$ is an uncomiited transaction and $T_{commited}$ indicates the set of commited transaction. A read operation $b \in OP_{T_i}$ MAY ONLY see the writes(changes) made by write operation $b$ that shares resources with $b$ AND also is subject to one of the following conditions:\\
33 \hspace{7mm} 1- $a \in OP_{T_j}$ ($j \neq i$) such that $T_j \in T_{commited}$ \\
35 \hspace{7mm} 2- $a \in OP_{T_i}$ and $a$ happens before $b$ in the natural order of the transaction. Formally, $a$ has a lower position than that of $b$ in $OP_{T_i}$ = \{$OP_1$, ..., $OP_n$\} \\
38 Def 6- \emph{Precedence Relationship for Read-Write Operations}: Assume $b$ is a read operation and $a$ is a write operation, and $a$ and $b$ share resource $r_i$, $a$ precedes $b$ ($a \rightarrow b$) if complying with Def 5, $b$ is allowed to see the writes to $r_i$ made by $a$. Otherwise, $b \rightarrow a$. For other pairs of operations or read-writes that do not share resources $a \rightarrow b$ and $b \rightarrow a$.\\
41 Corrolary 1- \emph{Read Must See Most Recent Comitted Write}: If $a \in OP{T_i}$ reads the resource $r_i$, in case $a$ has multiple 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} \in OP_{precedessors-for-r_i}$ such that $T_j$ has the greatest "commit instant" between all transaction with such operations. Otherwise, $a$ sees the most recent precedessor in $OP_{T_i}$. \\
43 proof: Consider case 1 that all precedessors are from sets of operations other than that of $a$'s, according to Def 4 all these prcedessors belong to comitted transactions. Assume $T_i$ is accessing data at $t_i$, $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 1 been already reflected in the file system. Since, $T_{i-1}$ has the greatest commit instant its changes have overriiden that of previously commited transactions and thus, $a$ reading $r_i$ from file system sees these changes.\\
45 In case 2 that there are operations 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$.\\
48 %Def 8- \emph{Precedence Relationship for Other Types of Operations}: Follwoing rules are ONLY enforced if precedence relationship is not detemined between two operations by Def 6. 1-If $T_i$ and $T_j$ are two transactions both committed with commit instant of $T_j$ being greater than commit instant of $T_i$ then $\forall op_i \in OP_{T_i}, \forall op_j \in OP_{T_j} op_i \rightarrow op_j$. 2-If two operation belong to the same transaction, then the one that occurs earlier in natural order of transaction precedes the other. 3- If $T_i$ is committed and $T_j$ is not, $\forall op_i \in OP_{T_i}, \forall op_j \in OP_{T_j} op_i \rightarrow op_j$. 4- If neither $T_i$ has commited nor $T_j$, then $\forall op_i \in OP_{T_i}, \forall op_j \in OP_{T_j} op_i \rightarrow op_j$, if there is either not a precedence relationship between $op_i$ and $op_j$ OR it is $op_i \rightarrow op_j$. 5- Otherwise, it means some operations in $T_i$ precede some of thos in $T_j$ and the other way around, for thos pairs not having such relationship it is assigned arbitrarily.\\
50 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$ $\rightarrow T_j$ \hspace{8mm} (this defines precedes relationship for members of $T$) \\
52 Def 8- 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 behavior of the program.\\
54 Corrolary 2: \emph{Upon Commit All Mebers of $T_{commit}$ Should Precede $T_i$}
56 proof: Follows imeediately from Def 8 and Def 9. This is later proven formally.i\\
58 %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. \\
60 %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$ sees the changes made by $op_i$ unless data has been changed by a more recent precedessor. Furthermore \\
62 %Def 5- Succeds relationship is defined similarly. \\
64 %Def 5- \emph{Precedence Relationship for Operations}: Assume $b$ is a read operation and $a$ is a write operation, and $a$ and $b$ share resource $r_i$, 1- if $b$ see the writes made by the $a$ to $r_i$ and their relationship conforms to Def 4, then $a$ precedes $b$ ($a \rightarrow b$) 2- if $b$ does not see the changes written by $a$, however their relatioship conforms to Def 4, $r_i$ has been changed by operation $c$ such that $t_{a-commit-instant}<t_{c-commint-instant}$ and $b$ sees the write made by $c$, then $a \rightarrow b$. 3- If $b$ does not see the changes made by $a$ and $r_i$ has been changed by operation $c$ such that 3- Otherwise $b$ precedes $a$. Precedence is only defined for a read and write operation sharing resources.\\
66 %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$. \\
71 %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: \\
73 %Rule 1- for any pair of operations (transactions) $a$ and $b$ their relationship is taken from the set \{$\rightarrow$, $\leftarrow$, $\leftarrow$ and $\rightarrow$\} \\
75 %proof: Follows from defenition. \\
77 %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}$. \\
79 %proof: the first part follows from Def 4 , second derives from Def 4 and second part of Def 1.\\
81 %Rule 1- $\forall op_i \in OP{T_i}$, $\forall op_j \in OP{T_j}$, $\forall op_k \in OP{T_k}$, if there is a precedence relationship between $op_i$ and $op_k$ sand $op_i \rightarrow op_k$, and if there is a relationship between $op_k$ and $op_j$ and $op_k \rightarrow op_j$, then $op_i \rightarrow op_j$ \\
83 %proof: Follows from the defenition of $\rightarrow$ \\
86 Rule 1- if $T_i \rightarrow T_k$ and $T_k \rightarrow T_j$ then $T_i \rightarrow T_j$ \\
88 proof: Since Def 9 ensures all operations in $OP_{T_i}$ precede those in $OP_{T_j}$. \\
90 Rule 2- 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 all members of $T_{commited}$ should precede $T_j$ (hence they should succed)\\
92 proof: $T_i$ denotes the last commited member of $T_{commited}$. Lets assume on the contrary $T_i$ does not precede $T_j$ and hence $T_j \rightarrow T_i$.\\
94 If there is not a pair of (read, write) or (write, read), sharing resource $r_n$ in the two transaction, then $T_i \rightarrow T_j$ according to Def 7 and Def 9.\\
96 If there are such operations, 1-At least an operation $a$ reads from $r_n$ in $OP_i$ sees the writes made by a write operation on $r_n$($b$) in $OP_j$, however since $T_j$ is just about to commit and acording to Def 4, writes are not reflected till commit instant, hence $a$ could not have read the writes made by $b$ and consequently $a$ does not precede $b$ contradicting the assumption $T_j \rightarrow T_i$ . OR 2- An operation $a$ in $T_i$ writes to resource $r_i$ and operation $b$ in $T_j$ reads resource $b$, according to Def 5 and Def 5 $a$ precedes $b$ and $b$ does not precede $a$, hence contradicting the assumption that $T_j \rightarrow T_i$.\\
99 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_{i-1}$ precedes $T_i$ and $T_i$ precedes $T_{j}$, hence $T_{i-1}$ precedes $T_{j}$. Same reasoning is applied for all the members of $T_{commited}$. \\
101 %If an operation $op_{i_1}$ in $OP_i$, writes 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. \\
106 Rule 3- 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_{all}$ should precede $op_{i}$.\\
108 Follows immediately from Rule 2 and Def 7.
110 \subsection{TransactionalFile Opeartions}
111 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. \\
114 A Transactionalfile can be shared among any subset of the members of $T$. If shared, the offset is shared between these too.
116 \section{Implications for the System}
118 \subsection{General Implications}
119 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. \\
122 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 \in OP_{T_j}$ and an operation $a \in 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. \\
124 %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.)\\
127 %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.\\
129 %Principle 0: An operation should not see any modifications other than those made by precedessors (either in the same transaction or others)\\
131 proof: Obviously such modifications are not valid and are probably part of a faulty operation.\\
134 Principle 1) If an operation $a$ that "reads" some data $r_n$ (reads the data at some $t < t_{commit-of-the-transaction}$(the commit instant)), it should be ensured that the data $r_n$ is still valid in the actual file system at $t_{commit-of-the-transaction}$ (commit instant) or $T_i$ has to abort.\\
136 proof: If the data is not valid anymore it means the data $r_n$ has been written since $t_{i-1}$. This implies at least one operation $b$ has written the data since the use and $b$ does not precede $a$ and $a$ precedes $b$. $b$ is either an operation in the same transaction or a different one. According to Def 4, 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 so it is still valid at commit instant. Hence, $b$ belongs to a different transaction namely $T_j$. Since $T_j$ should have already commited, according to Rule 3 all operation in $OP_{T_j}$ should precede those in $OP_{T_i}$, however, we know there is at least an operation $b$ that does not precede $a$ (since $a$ has not seen the "writes" made to $r_n$ by $b$). Hence, $T_i$ can not commit.\\
139 %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).\\
141 %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.\\
143 %rinciple 3) 1- A read operation in $OP_{T_i}$ "uses" contents read and makes $T_i$ dependent on the file contents read.\\
145 %proof: Due to assumption 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\\
147 %Principle 4) 1- A write operation in $OP_{T_i}$ does not make $T_i$ dependent on file contents.\\
149 %proof: The result of a write would always be the same contents thus, according to Def 2 does not count as using.\\
151 \subsection{A Model for Offset and Data Dependeny for Operations}
153 %Assumption: Each operation has a offset status assioated with it. We call this operation.offsetstatus. Each operation has a data satus assosiated with it namely operation.datastatus\\
155 %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 transaction and not being valid at commit instant\\
157 %Assumption: Based on previous assumptions read.datastatus = Defenite and others are Speculative, hence they do not use the "file contents"
159 %Principle 5: an operation with defeinte offset status assosiated with it is the only one "using" the offset value.\\
161 %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.\\
166 %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. \\
168 %1- $f$(Seek) = Absolute
170 %proof: seek operation does not invlove reading offset value hence, according to assumptions it is considered as absoulute.\\
172 %2-$f$(Read) = Defenite
174 %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.\\
176 %3-$f$(Write) = Speculative
178 %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.\\
180 %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:\\
182 %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 \\
184 %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.\\
186 %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.\\
188 %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\\
190 %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.\\
192 %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.\\
194 %Req 3: Any operation with offsetstaus = Defenite, should change the offsetstatus for prveious operations with a value of Speculative, to Defenite.\\
196 %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.\\
198 %Req 4: Any operation $op$ which applying $f$ on it yields in Speculative has offsettype=Speculative unless specified otherwise by previous requirements.\\
200 %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.\\
202 %Req 5: An operation with datastatus = Defenite, converts all the speculative offsttypes of the previous operations to Defenite. This requirement is always enforced.\\
204 proof: Since if datastatus = Defenite, this mean the operation is "using" or "reading" some file contents- an irreversible action- and as this operation should be able to see the modifications made by all preceding operations, if these are speculative, at commit instant they may "relocate" their modifications, this means eitehr $op$ may not see some changes made by precedessors or may see some changes not made by any precedessors (since the speculatively changes were used by $op$ however these did not get reflected in the actual file system since they were relocated at commit instant). Either way contradicts the defenitions and principles (Def 8 and Principle 0).\\
206 Note: Req 5 suggest if datatype = Definite this causes all the previous operation with Speculative as offsettype to be changed to Defenite.
208 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:\\
210 1- if $f(operation) = Absolute$, $g(offsetstat_1, ..., {offsetstat_{n-1}}, operation) = ({offsetstat_1}, ..., {offsetstat_{n-1}}, Absolute)$ leaving all offsetstats intact.\\
212 2- if $f(operation) = Defenite$:\\
215 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.\\
218 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)$)\\
220 3- if $f(operation) = Speculative$:\\
223 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.\\
226 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)$\\
229 3.3- else $g(offsetstat_1, ..., offsetstat_{n-1}, operation) = (offsetstat_1, ..., offsetstat_{n-1}, Speculative)$\\
231 4- After doing the above check if datastatus = Defenite, then change all offsettypes in the input that are Speculative to Defenite in the output.
233 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. 4 also ensures Req 5.
242 %$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, \}
246 %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.
248 %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.\\
249 %According to priciple 1 the offset chosen should be validated at the the commit instant.\\
250 \section{Implementation Overview}
252 %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.
253 Now we will describe the components of our system and demosntrate how the algorithm conforms to the function just described, and how all the rules principles are gurantedd.
265 %\begin{tabular}{c|c|c|}
projects / IRC.git / blob