*** empty log message ***
[IRC.git] / Robust / Transactions / Notes / sysgurantees.tex
1 \documentclass[a4paper, 11pt]{article}
2 \begin{document}
3 \section{Requirements}
4 \subsection{Transactions}
5 We have a set of Threads $T$ each representing a transaction.The code for a 
6 Transaction is like below:
7
8 \hspace{12mm}   Thread.doIt(new Callable)()\{
9
10 \hspace{12mm}           // code for transaction
11
12 \hspace{12mm}   \}
13
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. \\ 
16
17 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$. \\
18
19 \subsection{Defenitions}
20
21 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 \\
22
23 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. \\   
24
25 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.\\ 
26
27 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  \\ 
28
29 Def 5- Succeds relationship is defined similarly.  \\
30
31 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$. \\ 
32
33 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$) \\
34
35 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$
36
37 \subsection{Rules}
38 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: \\ 
39
40 Rule 1- for any pair of operations (transactions) $a$ and $b$ their relationship is taken from the set \{$\rightarrow$, $\leftarrow$, $\leftarrow$ and $\rightarrow$\} \\
41
42 proof: Follows from defenition. \\
43
44 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}$. \\  
45
46 proof: the first part follows from Def 4 , second derives from Def 4 and second part of Def 1.\\
47
48 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$ \\
49
50 proof: Follows from the defenition of $\rightarrow$ \\
51
52
53 Rule 4- if $T_i \rightarrow T_k$ and $T_k \rightarrow T_j$ then $T_i \rightarrow T_j$ \\
54
55 proof: Follows from Rule 2 and Def 7. \\ 
56
57
58 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)\\
59
60 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$. \\ 
61
62 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. \\
63
64
65 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}$. \\ 
66
67
68 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)\\
69
70 Follows immediately from rule 4 and def 7. 
71
72 \subsection{TransactionalFile Opeartions}
73 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. \\
74
75
76 A Transactionalfile can be shared among any subset of the members of $T$. If shared, the offset is shared between these too. 
77
78 \section{Implications for the System}
79 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. \\
80
81
82 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. \\
83
84 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.)\\
85
86
87 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.
88
89
90 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.//
91
92 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.\\
93
94
95 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).\\
96
97 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.\\ 
98
99 Principle 3) 1- A read operation in $OP_{T_i}$ "uses" contents read and makes $T_i$ dependent on the file contents read.\\
100
101 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\\
102
103 Principle 4) 1- A write operation in $OP_{T_i}$ does not make $T_i$ dependent on file contents.\\   
104
105 proof: The result of a write would always be the same contents thus, according to Def 2 does not count as using.\\
106
107 Assumption: Each operation has an offset status assioated with it. We call this operation.offsetstatus\\
108
109 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. \\
110
111 Principle 5: an operation with defeinte offset status assosiated with it is the only one "using" the offset value.\\
112
113 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.\\ 
114
115
116
117
118 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. \\
119
120 1- $f$(Seek) = Absolute 
121
122 proof: seek operation does not invlove reading offset value hence, according to assumptions it is considered as absoulute.\\
123
124 2-$f$(Read) = Defenite
125
126 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.\\
127
128 3-$f$(Write) = Speculative
129
130 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.\\   
131
132 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:\\
133
134 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 \\
135
136 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.\\
137
138 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.\\
139
140 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\\
141
142 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.\\
143
144 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. 
145
146 Req 3: Any operation with offsetstaus = Defenite, should change the offsetstatus for prveious operations with a value of Speculative, to Defenite.\\
147
148 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.\\
149
150 Req 4: Any operation $op$ which applying $f$ on it yields in Speculative has offsettype=Speculative unless specified otherwise by previous requirements.\\
151
152 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.\\ 
153
154
155 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:\\
156
157 1- if $f(operation) = Absolute$, $g(offsetstat_1, ..., {offsetstat_{n-1}}, operation) = ({offsetstat_1}, ..., {offsetstat_{n-1}}, Absolute)$ leaving all offsetstats intact.\\
158
159 2- if $f(operation) = Defenite$:\\
160
161 \hspace{ 8mm}
162         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.\\ 
163
164 \hspace{ 8mm}
165         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)$)\\
166
167 3- if $f(operation) = Speculative$:\\
168
169 \hspace{ 8mm}
170         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.\\ 
171
172 \hspace{ 8mm}
173         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)$\\
174
175 \hspace{ 8mm}
176         3.3- else $g(offsetstat_1, ..., offsetstat_{n-1}, operation) = (offsetstat_1, ..., offsetstat_{n-1}, Speculative)$\\
177
178
179 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.  
180
181
182
183
184
185
186
187
188 %$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, \}
189
190
191
192 %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.
193
194 %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.\\
195 %According to priciple 1 the offset chosen should be validated at the the commit instant.\\
196 \section{Implementation Overview}
197
198 %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. 
199 Now we will describe the components of our system and demosntrate how the algorithm 
200
201
202
203
204
205
206
207
208
209 to be continued
210
211 %\begin{tabular}{c|c|c|}
212 \end{document}