diff --git a/Recherche/ALDLoverAB/algo/index.tex b/Recherche/ALDLoverAB/algo/index.tex index 96385b7..b7e5fc2 100644 --- a/Recherche/ALDLoverAB/algo/index.tex +++ b/Recherche/ALDLoverAB/algo/index.tex @@ -1,60 +1,59 @@ -We consider a set of processes communicating asynchronously over reliable point-to-point channels. Each process maintains the following shared variables: +We consider a set of processes communicating asynchronously over reliable point-to-point channels. Each process maintains the following local or shared variables: \begin{itemize} - \item \textbf{received}: the set of messages received (but not yet delivered). - \item \textbf{delivered}: the set of messages that have been received, ordered, and delivered. - \item \textbf{prop[$r$][$j$]}: the proposal set of process $j$ at round $r$. It contains the set of messages that process $j$ claims to have received but not yet delivered at round $r$, concatenated with its newly broadcast message. - \item \textbf{proves}: the current content of the \texttt{DenyList} registry, accessible via the operation \texttt{READ()}. It returns a list of tuples $(j, \texttt{PROVE}(r))$, each indicating that process $j$ has issued a valid \texttt{PROVE} for round $r$. - \item \textbf{winner$^r$}: the set of processes that have issued a valid \texttt{PROVE} operation for round $r$. - \item \textbf{RB-cast}: a reliable broadcast primitive that satisfies the properties defined in Section~1.1.2. - \item \textbf{APPEND$(r)$}, \textbf{PROVE$(r)$}: operations that respectively insert (APPEND) and attest (PROVE) the participation of a process in round $r$ in the DenyList registry. - \item \textbf{READ()}: retrieves the current local view of valid operations (APPENDs and PROVEs) from the DenyList. - \item \textbf{ordered$(S)$}: returns a deterministic total order over a set $S$ of messages (e.g., via hash or lexicographic order). + \item \textbf{\textit{received}}: the set of messages that have been received via the reliable broadcast primitive but not yet ordered. + \item \textbf{\textit{delivered}}: the set of messages that have been ordered. + \item \textbf{\textit{prop}[$r$][$j$]}: the proposal set announced by process $j$ at round $r$. It contains a set of messages that process $j$ claims to have received but not yet delivered. + \item \textbf{\textit{winner}$^r$}: the set of processes that have issued a valid \texttt{PROVE} for round $r$, as observed through the registry. + \item \textbf{\texttt{RB-cast}$(\texttt{PROP}, S, r, j)$}: a reliable broadcast invocation that disseminates the proposal $S$ from process $j$ for round $r$. + \item \textbf{\texttt{RB-delivered}$(\texttt{PROP}, S, r, j)$}: the handler invoked upon reception of a \texttt{RB-cast}, which stores the received proposal $S$ into $\textit{prop}[r][j]$. + \item \textbf{\texttt{READ}()} : returns the current view of all valid operations stored in the DenyList registry. + \item \textbf{\texttt{ordered}$(S)$}: returns a deterministic total order over a set $S$ of messages. \end{itemize} \resetalgline \begin{algorithm} - - \vspace{1em} - \textbf{RB-received$(m, S, r_0, j_0)$} + \caption{Atomic Broadcast with DenyList} \begin{algorithmic}[1] - \State \nextalgline $\textit{received} \gets \textit{received} \cup \{m\}$ - \State \nextalgline $\textit{prop}[r_0][j_0] \gets S$ - \end{algorithmic} + \State $\textit{proves} \gets \emptyset$ + \State $\textit{received} \gets \emptyset$ + \State $\textit{delivered} \gets \emptyset$ + \State $r_1 \gets 0$ - \vspace{1em} - \textbf{AB-broadcast$(m, j_0)$} - \begin{algorithmic}[1] - \State \nextalgline $\textit{proves} \gets \texttt{READ}()$ - \State \nextalgline $r_0 \gets \max\{r : \exists j,\ (j, \texttt{PROVE}(r)) \in \textit{proves}\} + 1$ - \State \nextalgline $\texttt{RB-cast}(m, (\textit{received} \setminus \textit{delivered}) \cup \{m\}, r_0, j_0)$ - \State \nextalgline \texttt{PROVE}$(r_0)$ - \State \nextalgline \texttt{APPEND}$(r_0)$ - \Repeat - \State \nextalgline $\textit{proves} \gets \texttt{READ}()$ - \State \nextalgline $r_1 \gets \max\{r : \exists j,\ (j, \texttt{PROVE}(r)) \in \textit{proves}\} - 1$ - \State \nextalgline $\textit{winner}^{r_1} \gets \{j : (j, \texttt{PROVE}(r_1)) \in \textit{proves}\}$ - \State \nextalgline \textbf{wait} $\forall j \in \textit{winner}^{r_1},\ \textit{prop}[r_1][j] \neq \bot$ - \Until{\nextalgline $\forall r_2,\ \exists j_2 \in \textit{winner}^{r_2},\ m \in \textit{prop}[r_2][j_2]$} \nextalgline - \end{algorithmic} + \vspace{1em} + % --- AB-Broadcast --- + \State \nextalgline \textbf{AB-Broadcast}$_j(m)$ + \State \nextalgline \hspace{1em} $\texttt{RB-Broadcast}_j(m)$ + + \vspace{1em} + % --- RB-delivered --- + \State \nextalgline \textbf{RB-delivered}$_j(m)$ + \State \nextalgline \hspace{1em} $\textit{received} \gets \textit{received} \cup \{m\}$ + \State \nextalgline \hspace{1em} \textbf{repeat until} $\textit{received} \setminus \textit{delivered} \neq \emptyset$ + \State \nextalgline \hspace{2em} $S \gets \textit{received} \setminus \textit{delivered}$ + \State \nextalgline \hspace{2em} $\textit{proves} \gets \texttt{READ}()$ + \State \nextalgline \hspace{2em} $r_2 \gets \max\{r : j,\ (j, \texttt{PROVE}(r)) \in \textit{proves}\} + 1$ + \State \nextalgline \hspace{2em} $\texttt{RB-cast}(\texttt{PROP}, S, r_2, j)$ + \State \nextalgline \hspace{2em} $\texttt{PROVE}(r_2)$ + + \vspace{0.5em} + \State \nextalgline \hspace{2em} \textbf{for } $r \in [r_1 + 1, \dots, r_2]$ \textbf{do} + \State \nextalgline \hspace{3em} $\texttt{APPEND}(r)$ + \State \nextalgline \hspace{3em} $\textit{proves} \gets \texttt{READ}()$ + \State \nextalgline \hspace{3em} $\textit{winner}^r \gets \{j : (j, \texttt{PROVE}(r)) \in \textit{proves}\}$ + \State \nextalgline \hspace{3em} \textbf{wait } $\forall j \in \textit{winner}^r,\ \textit{prop}[r][j] \neq \bot$ + \State \nextalgline \hspace{3em} $T \gets \bigcup_{j \in \textit{winner}^r} \textit{prop}[r][j] \setminus \textit{delivered}$ + + \vspace{0.5em} + \State \nextalgline \hspace{3em} \textbf{for each } $m \in \texttt{ordered}(T)$ + \State \nextalgline \hspace{4em} $\textit{delivered} \gets \textit{delivered} \cup \{m\}$ + \State \nextalgline \hspace{4em} $\texttt{AB-deliver}_j(m)$ + \State \nextalgline \hspace{2em} $r_1 \gets r_2$ + + \vspace{1em} + % --- RB-deliver(Prop) handler --- + \State \nextalgline \textbf{RB-delivered}$_j(\texttt{PROP}, S, r_1, j_1)$ + \State \nextalgline \hspace{1em} $\textit{prop}[r_1][j_1] \gets S$ - \vspace{1em} - \textbf{AB-listen} - \begin{algorithmic}[1] - \While{true} - \State \nextalgline $\textit{proves} \gets \texttt{READ}()$ - \State \nextalgline $r_1 \gets \max\{r : \exists j,\ (j, \texttt{PROVE}(r)) \in \textit{proves}\} - 1$ - \For{$r_2 \in [r_0, \dots, r_1]$} \nextalgline - \State \nextalgline \texttt{APPEND}$(r_2)$ - \State \nextalgline $\textit{proves} \gets \texttt{READ}()$ - \State \nextalgline $\textit{winner}^{r_2} \gets \{j : (i, \texttt{PROVE}(r_2)) \in \textit{proves}\}$ - \State \nextalgline \textbf{wait} $\forall j \in \textit{winner}^{r_2},\ \textit{prop}[r_2][j] \neq \bot$ - \State \nextalgline $M^{r_2} \gets \bigcup_{j \in \textit{winner}^{r_2}} \textit{prop}[r_2][j]$ - \ForAll{$m \in \texttt{ordered}(M^{r_2})$} \nextalgline - \State \nextalgline $\textit{delivered} \gets \textit{delivered} \cup \{m\}$ - \State \nextalgline \texttt{AB-deliver}$(m)$ - \EndFor - \EndFor - \EndWhile \end{algorithmic} \end{algorithm} \ No newline at end of file diff --git a/Recherche/ALDLoverAB/main.bcf b/Recherche/ALDLoverAB/main.bcf new file mode 100644 index 0000000..f084873 --- /dev/null +++ b/Recherche/ALDLoverAB/main.bcf @@ -0,0 +1,2416 @@ + + + + + + output_encoding + utf8 + + + input_encoding + utf8 + + + debug + 0 + + + mincrossrefs + 2 + + + minxrefs + 2 + + + sortcase + 1 + + + sortupper + 1 + + + + + + + alphaothers + + + + + extradatecontext + labelname + labeltitle + + + labelalpha + 0 + + + labelnamespec + shortauthor + author + shorteditor + editor + translator + + + labeltitle + 0 + + + labeltitlespec + shorttitle + title + maintitle + + + labeltitleyear + 0 + + + labeldateparts + 0 + + + labeldatespec + date + year + eventdate + origdate + urldate + nodate + + + julian + 0 + + + gregorianstart + 1582-10-15 + + + maxalphanames + 3 + + + maxbibnames + 3 + + + maxcitenames + 3 + + + maxsortnames + 3 + + + maxitems + 3 + + + minalphanames + 1 + + + minbibnames + 1 + + + mincitenames + 1 + + + minsortnames + 1 + + + minitems + 1 + + + nohashothers + 0 + + + noroman + 0 + + + nosortothers + 0 + + + pluralothers + 0 + + + singletitle + 0 + + + skipbib + 0 + + + skipbiblist + 0 + + + skiplab + 0 + + + sortalphaothers + + + + + sortlocale + french + + + sortingtemplatename + nty + + + sortsets + 0 + + + uniquelist + false + + + uniquename + false + + + uniqueprimaryauthor + 0 + + + uniquetitle + 0 + + + uniquebaretitle + 0 + + + uniquework + 0 + + + useprefix + 0 + + + useafterword + 1 + + + useannotator + 1 + + + useauthor + 1 + + + usebookauthor + 1 + + + usecommentator + 1 + + + useeditor + 1 + + + useeditora + 1 + + + useeditorb + 1 + + + useeditorc + 1 + + + useforeword + 1 + + + useholder + 1 + + + useintroduction + 1 + + + usenamea + 1 + + + usenameb + 1 + + + usenamec + 1 + + + usetranslator + 0 + + + useshortauthor + 1 + + + useshorteditor + 1 + + + + + + extradatecontext + labelname + labeltitle + + + labelalpha + 0 + + + labelnamespec + shortauthor + author + shorteditor + editor + translator + + + labeltitle + 0 + + + labeltitlespec + shorttitle + title + maintitle + + + labeltitleyear + 0 + + + labeldateparts + 0 + + + labeldatespec + date + year + eventdate + origdate + urldate + nodate + + + maxalphanames + 3 + + + maxbibnames + 3 + + + maxcitenames + 3 + + + maxsortnames + 3 + + + maxitems + 3 + + + minalphanames + 1 + + + minbibnames + 1 + + + mincitenames + 1 + + + minsortnames + 1 + + + minitems + 1 + + + nohashothers + 0 + + + noroman + 0 + + + nosortothers + 0 + + + singletitle + 0 + + + skipbib + 0 + + + skipbiblist + 0 + + + skiplab + 0 + + + uniquelist + false + + + uniquename + false + + + uniqueprimaryauthor + 0 + + + uniquetitle + 0 + + + uniquebaretitle + 0 + + + uniquework + 0 + + + useprefix + 0 + + + useafterword + 1 + + + useannotator + 1 + + + useauthor + 1 + + + usebookauthor + 1 + + + usecommentator + 1 + + + useeditor + 1 + + + useeditora + 1 + + + useeditorb + 1 + + + useeditorc + 1 + + + useforeword + 1 + + + useholder + 1 + + + useintroduction + 1 + + + usenamea + 1 + + + usenameb + 1 + + + usenamec + 1 + + + usetranslator + 0 + + + useshortauthor + 1 + + + useshorteditor + 1 + + + + + datamodel + labelalphanametemplate + labelalphatemplate + inheritance + translit + uniquenametemplate + namehashtemplate + sortingnamekeytemplate + sortingtemplate + extradatespec + extradatecontext + labelnamespec + labeltitlespec + labeldatespec + controlversion + alphaothers + sortalphaothers + presort + texencoding + bibencoding + sortingtemplatename + sortlocale + language + autolang + langhook + indexing + hyperref + backrefsetstyle + block + pagetracker + citecounter + citetracker + ibidtracker + idemtracker + opcittracker + loccittracker + labeldate + labeltime + dateera + date + time + eventdate + eventtime + origdate + origtime + urldate + urltime + alldatesusetime + alldates + alltimes + gregorianstart + autocite + notetype + uniquelist + uniquename + refsection + refsegment + citereset + sortlos + babel + datelabel + backrefstyle + arxiv + familyinits + giveninits + prefixinits + suffixinits + useafterword + useannotator + useauthor + usebookauthor + usecommentator + useeditor + useeditora + useeditorb + useeditorc + useforeword + useholder + useintroduction + usenamea + usenameb + usenamec + usetranslator + useshortauthor + useshorteditor + debug + loadfiles + safeinputenc + sortcase + sortupper + terseinits + abbreviate + dateabbrev + clearlang + sortcites + sortsets + backref + backreffloats + trackfloats + parentracker + labeldateusetime + datecirca + dateuncertain + dateusetime + eventdateusetime + origdateusetime + urldateusetime + julian + datezeros + timezeros + timezones + seconds + autopunct + punctfont + labelnumber + labelalpha + labeltitle + labeltitleyear + labeldateparts + pluralothers + nohashothers + nosortothers + noroman + singletitle + uniquetitle + uniquebaretitle + uniquework + uniqueprimaryauthor + defernumbers + locallabelwidth + bibwarn + useprefix + skipbib + skipbiblist + skiplab + dataonly + defernums + firstinits + sortfirstinits + sortgiveninits + labelyear + isbn + url + doi + eprint + related + subentry + bibtexcaseprotection + mincrossrefs + minxrefs + maxnames + minnames + maxbibnames + minbibnames + maxcitenames + mincitenames + maxsortnames + minsortnames + maxitems + minitems + maxalphanames + minalphanames + maxparens + dateeraauto + + + alphaothers + sortalphaothers + presort + indexing + citetracker + ibidtracker + idemtracker + opcittracker + loccittracker + uniquelist + uniquename + familyinits + giveninits + prefixinits + suffixinits + useafterword + useannotator + useauthor + usebookauthor + usecommentator + useeditor + useeditora + useeditorb + useeditorc + useforeword + useholder + useintroduction + usenamea + usenameb + usenamec + usetranslator + useshortauthor + useshorteditor + terseinits + abbreviate + dateabbrev + clearlang + labelnumber + labelalpha + labeltitle + labeltitleyear + labeldateparts + nohashothers + nosortothers + noroman + singletitle + uniquetitle + uniquebaretitle + uniquework + uniqueprimaryauthor + useprefix + skipbib + skipbiblist + skiplab + dataonly + skiplos + labelyear + isbn + url + doi + eprint + related + subentry + bibtexcaseprotection + labelalphatemplate + translit + sortexclusion + sortinclusion + extradatecontext + labelnamespec + labeltitlespec + labeldatespec + maxnames + minnames + maxbibnames + minbibnames + maxcitenames + mincitenames + maxsortnames + minsortnames + maxitems + minitems + maxalphanames + minalphanames + + + noinherit + nametemplates + labelalphanametemplatename + uniquenametemplatename + namehashtemplatename + sortingnamekeytemplatename + presort + indexing + citetracker + ibidtracker + idemtracker + opcittracker + loccittracker + uniquelist + uniquename + familyinits + giveninits + prefixinits + suffixinits + useafterword + useannotator + useauthor + usebookauthor + usecommentator + useeditor + useeditora + useeditorb + useeditorc + useforeword + useholder + useintroduction + usenamea + usenameb + usenamec + usetranslator + useshortauthor + useshorteditor + terseinits + abbreviate + dateabbrev + clearlang + labelnumber + labelalpha + labeltitle + labeltitleyear + labeldateparts + nohashothers + nosortothers + noroman + singletitle + uniquetitle + uniquebaretitle + uniquework + uniqueprimaryauthor + useprefix + skipbib + skipbiblist + skiplab + dataonly + skiplos + isbn + url + doi + eprint + related + subentry + bibtexcaseprotection + maxnames + minnames + maxbibnames + minbibnames + maxcitenames + mincitenames + maxsortnames + minsortnames + maxitems + minitems + maxalphanames + minalphanames + + + nametemplates + labelalphanametemplatename + uniquenametemplatename + namehashtemplatename + sortingnamekeytemplatename + uniquelist + uniquename + familyinits + giveninits + prefixinits + suffixinits + terseinits + nohashothers + nosortothers + useprefix + + + nametemplates + labelalphanametemplatename + uniquenametemplatename + namehashtemplatename + sortingnamekeytemplatename + uniquename + familyinits + giveninits + prefixinits + suffixinits + terseinits + useprefix + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + prefix + family + + + + + shorthand + label + labelname + labelname + + + year + + + + + + labelyear + year + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + prefix + family + given + + + + family + given + prefix + suffix + + + + + prefix + family + + + given + + + suffix + + + prefix + + + mm + + + + sf,sm,sn,pf,pm,pn,pp + family,given,prefix,suffix + boolean,integer,string,xml + default,transliteration,transcription,translation + + + article + artwork + audio + bibnote + book + bookinbook + booklet + collection + commentary + customa + customb + customc + customd + custome + customf + dataset + inbook + incollection + inproceedings + inreference + image + jurisdiction + legal + legislation + letter + manual + misc + movie + music + mvcollection + mvreference + mvproceedings + mvbook + online + patent + performance + periodical + proceedings + reference + report + review + set + software + standard + suppbook + suppcollection + suppperiodical + thesis + unpublished + video + xdata + + + sortyear + volume + volumes + abstract + addendum + annotation + booksubtitle + booktitle + booktitleaddon + chapter + edition + eid + entrysubtype + eprintclass + eprinttype + eventtitle + eventtitleaddon + gender + howpublished + indexsorttitle + indextitle + isan + isbn + ismn + isrn + issn + issue + issuesubtitle + issuetitle + issuetitleaddon + iswc + journalsubtitle + journaltitle + journaltitleaddon + label + langid + langidopts + library + mainsubtitle + maintitle + maintitleaddon + nameaddon + note + number + origtitle + pagetotal + part + relatedstring + relatedtype + reprinttitle + series + shorthandintro + subtitle + title + titleaddon + usera + userb + userc + userd + usere + userf + venue + version + shorthand + shortjournal + shortseries + shorttitle + sorttitle + sortshorthand + sortkey + presort + institution + lista + listb + listc + listd + liste + listf + location + organization + origlocation + origpublisher + publisher + afterword + annotator + author + bookauthor + commentator + editor + editora + editorb + editorc + foreword + holder + introduction + namea + nameb + namec + translator + shortauthor + shorteditor + sortname + authortype + editoratype + editorbtype + editorctype + editortype + bookpagination + nameatype + namebtype + namectype + pagination + pubstate + type + language + origlanguage + crossref + xref + date + endyear + year + month + day + hour + minute + second + timezone + yeardivision + endmonth + endday + endhour + endminute + endsecond + endtimezone + endyeardivision + eventdate + eventendyear + eventyear + eventmonth + eventday + eventhour + eventminute + eventsecond + eventtimezone + eventyeardivision + eventendmonth + eventendday + eventendhour + eventendminute + eventendsecond + eventendtimezone + eventendyeardivision + origdate + origendyear + origyear + origmonth + origday + orighour + origminute + origsecond + origtimezone + origyeardivision + origendmonth + origendday + origendhour + origendminute + origendsecond + origendtimezone + origendyeardivision + urldate + urlendyear + urlyear + urlmonth + urlday + urlhour + urlminute + urlsecond + urltimezone + urlyeardivision + urlendmonth + urlendday + urlendhour + urlendminute + urlendsecond + urlendtimezone + urlendyeardivision + doi + eprint + file + verba + verbb + verbc + url + xdata + ids + entryset + related + keywords + options + relatedoptions + pages + execute + + + abstract + annotation + authortype + bookpagination + crossref + day + doi + eprint + eprintclass + eprinttype + endday + endhour + endminute + endmonth + endsecond + endtimezone + endyear + endyeardivision + entryset + entrysubtype + execute + file + gender + hour + ids + indextitle + indexsorttitle + isan + ismn + iswc + keywords + label + langid + langidopts + library + lista + listb + listc + listd + liste + listf + minute + month + namea + nameb + namec + nameatype + namebtype + namectype + nameaddon + options + origday + origendday + origendhour + origendminute + origendmonth + origendsecond + origendtimezone + origendyear + origendyeardivision + orighour + origminute + origmonth + origsecond + origtimezone + origyear + origyeardivision + origlocation + origpublisher + origtitle + pagination + presort + related + relatedoptions + relatedstring + relatedtype + second + shortauthor + shorteditor + shorthand + shorthandintro + shortjournal + shortseries + shorttitle + sortkey + sortname + sortshorthand + sorttitle + sortyear + timezone + url + urlday + urlendday + urlendhour + urlendminute + urlendmonth + urlendsecond + urlendtimezone + urlendyear + urlhour + urlminute + urlmonth + urlsecond + urltimezone + urlyear + usera + userb + userc + userd + usere + userf + verba + verbb + verbc + xdata + xref + year + yeardivision + + + set + entryset + + + article + addendum + annotator + author + commentator + editor + editora + editorb + editorc + editortype + editoratype + editorbtype + editorctype + eid + issn + issue + issuetitle + issuesubtitle + issuetitleaddon + journalsubtitle + journaltitle + journaltitleaddon + language + note + number + origlanguage + pages + pubstate + series + subtitle + title + titleaddon + translator + version + volume + + + bibnote + note + + + book + author + addendum + afterword + annotator + chapter + commentator + edition + editor + editora + editorb + editorc + editortype + editoratype + editorbtype + editorctype + eid + foreword + introduction + isbn + language + location + maintitle + maintitleaddon + mainsubtitle + note + number + origlanguage + pages + pagetotal + part + publisher + pubstate + series + subtitle + title + titleaddon + translator + volume + volumes + + + mvbook + addendum + afterword + annotator + author + commentator + edition + editor + editora + editorb + editorc + editortype + editoratype + editorbtype + editorctype + foreword + introduction + isbn + language + location + note + number + origlanguage + pagetotal + publisher + pubstate + series + subtitle + title + titleaddon + translator + volume + volumes + + + inbook + bookinbook + suppbook + addendum + afterword + annotator + author + booktitle + bookauthor + booksubtitle + booktitleaddon + chapter + commentator + edition + editor + editora + editorb + editorc + editortype + editoratype + editorbtype + editorctype + eid + foreword + introduction + isbn + language + location + mainsubtitle + maintitle + maintitleaddon + note + number + origlanguage + part + publisher + pages + pubstate + series + subtitle + title + titleaddon + translator + volume + volumes + + + booklet + addendum + author + chapter + editor + editortype + eid + howpublished + language + location + note + pages + pagetotal + pubstate + subtitle + title + titleaddon + type + + + collection + reference + addendum + afterword + annotator + chapter + commentator + edition + editor + editora + editorb + editorc + editortype + editoratype + editorbtype + editorctype + eid + foreword + introduction + isbn + language + location + mainsubtitle + maintitle + maintitleaddon + note + number + origlanguage + pages + pagetotal + part + publisher + pubstate + series + subtitle + title + titleaddon + translator + volume + volumes + + + mvcollection + mvreference + addendum + afterword + annotator + author + commentator + edition + editor + editora + editorb + editorc + editortype + editoratype + editorbtype + editorctype + foreword + introduction + isbn + language + location + note + number + origlanguage + publisher + pubstate + subtitle + title + titleaddon + translator + volume + volumes + + + incollection + suppcollection + inreference + addendum + afterword + annotator + author + booksubtitle + booktitle + booktitleaddon + chapter + commentator + edition + editor + editora + editorb + editorc + editortype + editoratype + editorbtype + editorctype + eid + foreword + introduction + isbn + language + location + mainsubtitle + maintitle + maintitleaddon + note + number + origlanguage + pages + part + publisher + pubstate + series + subtitle + title + titleaddon + translator + volume + volumes + + + dataset + addendum + author + edition + editor + editortype + language + location + note + number + organization + publisher + pubstate + series + subtitle + title + titleaddon + type + version + + + manual + addendum + author + chapter + edition + editor + editortype + eid + isbn + language + location + note + number + organization + pages + pagetotal + publisher + pubstate + series + subtitle + title + titleaddon + type + version + + + misc + software + addendum + author + editor + editortype + howpublished + language + location + note + organization + pubstate + subtitle + title + titleaddon + type + version + + + online + addendum + author + editor + editortype + language + note + organization + pubstate + subtitle + title + titleaddon + version + + + patent + addendum + author + holder + location + note + number + pubstate + subtitle + title + titleaddon + type + version + + + periodical + addendum + editor + editora + editorb + editorc + editortype + editoratype + editorbtype + editorctype + issn + issue + issuesubtitle + issuetitle + issuetitleaddon + language + note + number + pubstate + series + subtitle + title + titleaddon + volume + yeardivision + + + mvproceedings + addendum + editor + editortype + eventday + eventendday + eventendhour + eventendminute + eventendmonth + eventendsecond + eventendtimezone + eventendyear + eventendyeardivision + eventhour + eventminute + eventmonth + eventsecond + eventtimezone + eventyear + eventyeardivision + eventtitle + eventtitleaddon + isbn + language + location + note + number + organization + pagetotal + publisher + pubstate + series + subtitle + title + titleaddon + venue + volumes + + + proceedings + addendum + chapter + editor + editortype + eid + eventday + eventendday + eventendhour + eventendminute + eventendmonth + eventendsecond + eventendtimezone + eventendyear + eventendyeardivision + eventhour + eventminute + eventmonth + eventsecond + eventtimezone + eventyear + eventyeardivision + eventtitle + eventtitleaddon + isbn + language + location + mainsubtitle + maintitle + maintitleaddon + note + number + organization + pages + pagetotal + part + publisher + pubstate + series + subtitle + title + titleaddon + venue + volume + volumes + + + inproceedings + addendum + author + booksubtitle + booktitle + booktitleaddon + chapter + editor + editortype + eid + eventday + eventendday + eventendhour + eventendminute + eventendmonth + eventendsecond + eventendtimezone + eventendyear + eventendyeardivision + eventhour + eventminute + eventmonth + eventsecond + eventtimezone + eventyear + eventyeardivision + eventtitle + eventtitleaddon + isbn + language + location + mainsubtitle + maintitle + maintitleaddon + note + number + organization + pages + part + publisher + pubstate + series + subtitle + title + titleaddon + venue + volume + volumes + + + report + addendum + author + chapter + eid + institution + isrn + language + location + note + number + pages + pagetotal + pubstate + subtitle + title + titleaddon + type + version + + + thesis + addendum + author + chapter + eid + institution + language + location + note + pages + pagetotal + pubstate + subtitle + title + titleaddon + type + + + unpublished + addendum + author + eventday + eventendday + eventendhour + eventendminute + eventendmonth + eventendsecond + eventendtimezone + eventendyear + eventendyeardivision + eventhour + eventminute + eventmonth + eventsecond + eventtimezone + eventyear + eventyeardivision + eventtitle + eventtitleaddon + howpublished + language + location + note + pubstate + subtitle + title + titleaddon + type + venue + + + abstract + addendum + afterword + annotator + author + bookauthor + booksubtitle + booktitle + booktitleaddon + chapter + commentator + editor + editora + editorb + editorc + foreword + holder + institution + introduction + issuesubtitle + issuetitle + issuetitleaddon + journalsubtitle + journaltitle + journaltitleaddon + location + mainsubtitle + maintitle + maintitleaddon + nameaddon + note + organization + origlanguage + origlocation + origpublisher + origtitle + part + publisher + relatedstring + series + shortauthor + shorteditor + shorthand + shortjournal + shortseries + shorttitle + sortname + sortshorthand + sorttitle + subtitle + title + titleaddon + translator + venue + + + article + book + inbook + bookinbook + suppbook + booklet + collection + incollection + suppcollection + manual + misc + mvbook + mvcollection + online + patent + periodical + suppperiodical + proceedings + inproceedings + reference + inreference + report + set + thesis + unpublished + + + date + year + + + + + set + + entryset + + + + article + + author + journaltitle + title + + + + book + mvbook + + author + title + + + + inbook + bookinbook + suppbook + + author + title + booktitle + + + + booklet + + + author + editor + + title + + + + collection + reference + mvcollection + mvreference + + editor + title + + + + incollection + suppcollection + inreference + + author + editor + title + booktitle + + + + dataset + + title + + + + manual + + title + + + + misc + software + + title + + + + online + + title + + url + doi + eprint + + + + + patent + + author + title + number + + + + periodical + + editor + title + + + + proceedings + mvproceedings + + title + + + + inproceedings + + author + title + booktitle + + + + report + + author + title + type + institution + + + + thesis + + author + title + type + institution + + + + unpublished + + author + title + + + + + isbn + + + issn + + + ismn + + + gender + + + + + + + sources.bib + + + + + + + presort + + + sortkey + + + sortname + author + editor + translator + sorttitle + title + + + sorttitle + title + + + sortyear + year + + + volume + 0 + + + + + + diff --git a/Recherche/ALDLoverAB/main.pdf b/Recherche/ALDLoverAB/main.pdf index c43fa0f..75a217e 100644 Binary files a/Recherche/ALDLoverAB/main.pdf and b/Recherche/ALDLoverAB/main.pdf differ diff --git a/Recherche/ALDLoverAB/main.tex b/Recherche/ALDLoverAB/main.tex index d8ca704..552cc04 100644 --- a/Recherche/ALDLoverAB/main.tex +++ b/Recherche/ALDLoverAB/main.tex @@ -41,9 +41,9 @@ \affil{Aix-Marseille Université, Scille} \date{\today} -\begin{titlepage} - \maketitle -\end{titlepage} +% \begin{titlepage} +% \maketitle +% \end{titlepage} \section{Introduction} diff --git a/Recherche/ALDLoverAB/proof/index.tex b/Recherche/ALDLoverAB/proof/index.tex index a41d896..e4bba0e 100644 --- a/Recherche/ALDLoverAB/proof/index.tex +++ b/Recherche/ALDLoverAB/proof/index.tex @@ -2,120 +2,106 @@ If a message $m$ is delivered by any process, then it was previously broadcast by some process via the \texttt{AB-broadcast} primitive. \end{theorem} + \begin{proof} - Let $j$ be a process such that $\text{AB-deliver}_j(m)$ occurs. + Let $j$ be a process such that $\texttt{AB-deliver}_j(m)$ occurs. \begin{align*} - &\text{AB-deliver}_j(m) & \text{(line 24)} \\ - \Rightarrow\; &\exists r_0 : m \in \texttt{ordered}(M^{r_0}) & \text{(line 22)} \\ - \Rightarrow\; &\exists j_0 : j_0 \in \textit{winner}^{r_0} \land m \in \textit{prop}[r_0][j_0] & \text{(line 21)} \\ - \Rightarrow\; &\exists m_0, S_0 : \text{RB-received}_{j_0}(m_0, S_0, r_0, j_0) \land m \in S_0 & \text{(line 2)} \\ - \Rightarrow\; &S_0 = (\textit{received}_{j_0} \setminus \textit{delivered}_{j_0}) \cup \{m_1\} & \text{(line 5)} \\ - \Rightarrow\; &\textbf{if } m_1 = m: \exists\, \text{AB-broadcast}_{j_0}(m) \hspace{1em} \square \\ - &\textbf{else if } m_1 \neq m: \\ - &\quad m \in \textit{received}_{j_0} \setminus \textit{delivered}_{j_0} \Rightarrow m \in \textit{received}_{j_0} \land m \notin \textit{delivered}_{j_0} \\ - &\quad \exists j_1, S_1, r_1 : \text{RB-received}_{j_1}(m, S_1, r_1, j_1) & \text{(line 1)} \\ - &\quad \Rightarrow \exists\, \text{AB-broadcast}_{j_1}(m) \hspace{1em} \square & \text{(line 5)} + &\texttt{AB-deliver}_j(m) & \text{(line 18)} \\ + \Rightarrow\; & m \in \texttt{ordered}(T),\ \text{with } T = \bigcup_{j' \in \textit{winner}^r} \textit{prop}[r][j'] \setminus \textit{delivered} & \text{(lines 16-17)} \\ + \Rightarrow\; & \exists j_0,\ r_0 : m \in \textit{prop}[r_0][j_0] & \text{(line 16)} \\ + \Rightarrow\; & \textit{prop}[r_0][j_0] = S,\ \text{with } \texttt{RB-delivered}_{j}(PROP, S, r_0, j_0) & \text{(line 22)} \\ + \Rightarrow\; & S \text{ was sent in } \texttt{RB-cast}(PROP, S, r_0, j_0) & \text{(line 9)} \\ + \Rightarrow\; & S = \textit{received}_{j_0} \setminus \textit{delivered}_{j_0} & \text{(line 6)} \\ + \Rightarrow\; & m' \in \textit{received}_{j_0}\ \text{where } m' \text{ broadcast by } j_0 & \text{(line 4)} \\ + \Rightarrow\; & \textbf{if } m = m' \\ + & \quad \Rightarrow \texttt{RB-Broadcast}_{j_0}(m) \text{ occurred} & \text{(line 3)} \\ + & \quad \Rightarrow \texttt{AB-Broadcast}_{j_0}(m) \text{ occurred} & \text{(line 1)} & \hspace{1em} \square \\ + & \textbf{else: } m \in \textit{received}_{j_0} \setminus \textit{delivered}_{j_0} \\ + & \quad \Rightarrow m \in \textit{received}_{j_0} & \text{(line 4)} \\ + & \quad \Rightarrow \texttt{RB-delivered}_{j_0}(m) \text{ occurred} & \text{(line 3)} \\ + & \quad \Rightarrow \exists j_1 : \texttt{RB-Broadcast}_{j_1}(m) \text{ occurred} & \text{(line 2)} \\ + & \quad \Rightarrow \texttt{AB-Broadcast}_{j_1}(m) \text{ occurred} & \text{(line 1)} & \hspace{1em} \square \end{align*} + + Therefore, every delivered message $m$ must originate from some call to \texttt{AB-Broadcast}. \end{proof} - - - \begin{theorem}[No Duplication] No message is delivered more than once by any process. \end{theorem} \begin{proof} - Let $j$ be a process such that both $\text{AB-deliver}_j(m_0)$ and $\text{AB-deliver}_j(m_1)$ occur, with $m_0 = m_1$. - + Assume by contradiction that a process $j$ delivers the same message $m$ more than once, i.e., + \[ + \texttt{AB-deliver}_j(m) \text{ occurs at least twice.} + \] + \begin{align*} - &\text{AB-deliver}_j(m_0) \wedge \text{AB-deliver}_j(m_1) & \text{(line 24)} \\ - \Rightarrow\; & m_0, m_1 \in \textit{delivered}_j & \text{(line 23)} \\ - \Rightarrow\; &\exists r_0, r_1 : m_0 \in M^{r_0} \wedge m_1 \in M^{r_1} & \text{(line 22)} \\ - \Rightarrow\; &\exists j_0, j_1 : m_0 \in \textit{prop}[r_0][j_0] \wedge m_1 \in \textit{prop}[r_1][j_1] \\ - &\hspace{2.5em} \wedge\ j_0 \in \textit{winner}^{r_0},\ j_1 \in \textit{winner}^{r_1} & \text{(line 21)} + &\texttt{AB-deliver}_j(m) \text{ occurs} & \text{(line 19)} \\ + \Rightarrow\; & m \in \texttt{ordered}(T),\ \text{where } T = \bigcup_{j' \in \textit{winner}^r} \textit{prop}[r][j'] \setminus \textit{delivered} & \text{(lines 16-17)} \\ + \Rightarrow\; & m \notin \textit{delivered} \text{ at that time} \\ + \\ + \text{However:} \\ + & \texttt{delivered} \gets \texttt{delivered} \cup \{m\} & \text{(line 18)} \\ + \Rightarrow\; & m \in \textit{delivered} \text{ permanently} \\ + \Rightarrow\; & \text{In any future round, } m \notin T' \text{ since } T' = \bigcup_{j' \in \textit{winner}^r} \textit{prop}[r'][j'] \setminus \textit{delivered} \\ + \Rightarrow\; & m \text{ will not be delivered again} \\ + \Rightarrow\; & \text{Contradiction.} \end{align*} - We now distinguish two cases: - - \vspace{0.5em} - \noindent\textbf{Case 1:} $r_0 = r_1$: - \begin{itemize} - \item If $j_0 \neq j_1$: this contradicts message uniqueness, since two different processes would include the same message in round $r_0$. - \item If $j_0 = j_1$: - \begin{align*} - \Rightarrow & |{(j_0, \texttt{PROVE}(r_0)) \in proves}| \geq 2 & \text{(line 19)}\\ - \Rightarrow &\texttt{PROVE}_{j_0}(r_0) \text{ occurs 2 times} & \text{(line 6)}\\ - \Rightarrow &\texttt{AB-Broadcast}_{j_0}(m_0) \text{ were invoked two times} \\ - \Rightarrow &(max\{r: \exists j, (j, \texttt{PROVE}(r)) \in proves\} + 1) & \text{(line 4)}\\ - &\text{ returned the same value in two differents invokations of \texttt{AB-Broadcast}} \\ - &\textbf{But } \texttt{PROVE}(r_0) \Rightarrow \texttt{max}\{r: \exists j, (j, \texttt{PROVE}(r)) \in proves\} + 1 > r_0 \\ - &\text{It's impossible for a single process to submit two messages in the same round} \hspace{1em} \\ - \end{align*} - \end{itemize} - - % \vspace{0.5em} - \noindent\textbf{Case 2:} $r_0 \ne r_1$: - \begin{itemize} - \item If $j_0 \neq j_1$: again, message uniqueness prohibits two different processes from broadcasting the same message in different rounds. - \item If $j_0 = j_1$: message uniqueness also prohibits the same process from broadcasting the same message in two different rounds. - \end{itemize} - - In all cases, we reach a contradiction. Therefore, it is impossible for a process to deliver the same message more than once. $\square$ + Therefore, no message can be delivered more than once by the same process. $\square$ \end{proof} -% \subsubsection{No Duplication} +\begin{theorem}[Validity] + If a correct process invokes $\texttt{AB-Broadcast}_j(m)$, then all correct processes eventually deliver $m$. +\end{theorem} + +\begin{proof} + Let $j$ be a correct process such that $\texttt{AB-Broadcast}_j(m)$ occurs (line 5). + + \begin{align*} + &\texttt{AB-Broadcast}_j(m) & \text{(line 1)}\\ + \Rightarrow\; & \texttt{RB-Broadcast}_j(m) \text{ occurs} & \text{(line 2)} \\ + \Rightarrow\; & \forall j_0 : \texttt{RB-delivered}_{j_0}(m) & \text{(line 3)} \\ + \Rightarrow\; & m \in \textit{received}_{j_0} & \text{(line 4)} \\ + \Rightarrow\; & \textbf{if } m \in \texttt{delivered}_{j_0} \\ + & \quad \Rightarrow \textit{delivered}_{j_0} \gets textit{delivered}_{j_0} \cup \{m\} & \text{(line 18)} \\ + & \quad \Rightarrow \texttt{AB-delivered}_{j_0}(m) & \text{(line 19)} & \hspace{1em} \square \\ + & \textbf{else } m \notin \textit{delivered}_{j_0} : \\ + & \quad \Rightarrow m \in S_{j_0}\ \text{since } S_{j_0} = \textit{receieved}_{j_0} \setminus \textit{delivered}_{j_0} & \text{(line 6)} \\ + & \quad \Rightarrow \exists r : \texttt{RB-cast}_{j_0}(texttt{PROP}, S_{j_0}, r, j_0) & \text{(line 9)} \\ + & \quad \quad \Rightarrow \forall j_1 : \texttt{RB-Deliver}_{j_1}(\texttt{PROP}, S_{j_0}, r, j_0)\ \text{occurs} & \text{(line 21)} \\ + & \quad \quad \Rightarrow \textit{prop}[r][j_0] = S_{j_0} & \text{(line 22)} \\ + & \quad \Rightarrow \exists j_2 \in j_0 : \texttt{PROVE}_{j_2}(r)\ \text{is valid} & \text{(line 10)} \\ + & \quad \Rightarrow j_2 \in textit{winner}^r & \text{(line 14)} \\ + & \quad \Rightarrow T_{j_0} \ni \textit{prop}[r][j_2] \setminus \textit{delivered}_{j_0} & \text{(line 16)} \\ + & \quad \Rightarrow T_{j_0} \ni S_{j_2} \setminus \textit{delivered}_{j_0} \ni m & \text{(line 16)} \\ + & \quad \Rightarrow \texttt{AB-deliver}_{j_0}(m) & \text{(line 19)} & \hspace{1em} \square \\ + \end{align*} -% $M = (\bigcup_{i \rightarrow |P|} AB\_receieved_{i}(m)), \not\exists m_0 m_1 \in M \text{s.t. } m_1 = m_2$ -% \\ -% Proof \\ -% \begin{align*} -% &\text{Soit } i, m_0, m_1 \text{ tels que } m_0 = m_1 \\ -% &\exists r_0,\ m_0 \in M^{r_0} \\ -% &\exists r_1,\ m_1 \in M^{r_1} \\ -% &\text{if } r_0 = r_1 \\ -% &\quad \exists j_0, j_1,\ \text{prop tq } \text{prop}[r_0][j_0] = m_0,\ \text{prop}[r_0][j_1] = m_1 \quad j_0, j_1 \in \text{winnner}^{r_0} \\ -% &\quad \text{if} j_0 \neq j_1 \\ -% &\quad\quad \text{On admet qu'il est impossible pour un processus de soumettre le même msg qu'un autre} \\ -% &\quad \text{if } j_0 = j_1 \\ -% &\quad\quad j_0 \text{ a émis son } \text{PROVE}(r_0) \text{ valide 2 fois}\\ -% &\quad\quad \text{Impossible si } j_0 \text{ correct} \\ -% &\text{else} \\ -% &\quad \exists j_0, j_1,\ \text{prop tq } \text{prop}[r_0][j_0] = m_0,\ \text{prop}[r_0][j_1] = m_1 \quad j_0, j_1 \in \text{winnner}^{r_0} \\ -% &\quad \text{if } j_0 \neq j_1 \\ -% &\quad\quad \text{On admet qu'il est impossible pour un processus de soumettre le même msg qu'un autre} \\ -% &\quad \text{if } j_0 = j_1 \\ -% &j_0 \text{ à emis et validé 2 fois le même messages a des rounds différents.}\\ -% &\text{On admet que deux message identiques soumis a des rounds différents ne peuvent être identiques} -% \end{align*} +\end{proof} -\subsubsection{Broadcast Validity} -$\exists j_0, m_0 \quad AB\_broadcast_{j_0}(m_0) \Rightarrow \forall j_1 \quad AB\_received_{j_1}(m_0)$ \\ +\begin{theorem}[Total Order] + If two correct processes deliver two messages $m_1$ and $m_2$, then they deliver them in the same order. +\end{theorem} + +\begin{proof} + + \begin{align*} + & \forall j_0 : \texttt{AB-Deliver}_{j_0}(m_0) \wedge \texttt{AB-Deliver}_{j_0}(m_1) & \text{(line 19)} \\ + \Rightarrow\; & \exists r_0, r_1 : m_0 \in \texttt{ordered}(T^{r_0}) \wedge m_1 \in \texttt{ordered}(T^{r_1}) & \text{(line 17)} \\ + \Rightarrow\; & T^{r_0} = \bigcup_{j' \in \textit{winner}^{r_0}} \textit{prop}[r_0][j'] \setminus \textit{delivered}\ \wedge \\ + & T^{r_1} = \bigcup_{j' \in \textit{winner}^{r_1}} \textit{prop}[r_1][j'] \setminus \textit{delivered} & \text{(line 16)} \\ + \Rightarrow\; & \textbf{if } r_0 = r_1 \\ + & \quad \Rightarrow T^{r_0} = T^{r_1} \\ + & \quad \Rightarrow m_0, m_1 \in \texttt{ordered}(T^{r_0})\ \text{since \texttt{ordered} is deterministic} \\ + & \quad \Rightarrow \textbf{if } m_0 < m_1 : \\ + & \quad \quad \Rightarrow \texttt{AB-Deliver}_{j_0}(m_0) < \texttt{AB-Deliver}_{j_0}(m_1) & & \hspace{1em} \square\\ + & \textbf{else if } r_0 < r_1 \\ + & \quad \Rightarrow \forall m \in T^{r_0}, \forall m' \in T^{r_1} : \texttt{AB-Deliver}(m) < \texttt{AB-Deliver}(m') & & \hspace{1em} \square\\ + \end{align*} + + Therefore, for all correct processes, messages are delivered in the same total order. +\end{proof} -Proof: -\begin{align*} - &\exists j_0, m_0 \quad AB\_broadcast_{j_0}(m_0) \\ - &\forall j_1, \exists r_1 \quad RB\_deliver_{j_1}^{r_1}(m_0) \\ - &\exists receieved : m_0 \in receieved_{j_1} \\ - &\exists r_0 : RB\_deliver(PROP, r_0, m_0) & LOOP\\ - &\exists prop: \text{prop}[r_0][j_0] = m_0 \\ - &\text{if } \not\exists (j_0, PROVE(r_0)) \in \text{proves} \\ - &\quad r_0 += 1 \\ - &\quad \text{jump to LOOP} \\ - &\text{else} \\ - &\quad \exists \text{winner}, \text{winner}^{r_0} \ni j_0 \\ - &\quad \exists M^{r_0} \ni (\text{prop}[r_0][j_0] = m_0) \\ - &\quad \forall j_1, \quad AB\_deliver_{j_1}(m_0) -\end{align*} - -\subsubsection*{AB receive width} -\[ -\exists j_0, m_0 \quad AB\_deliver_{j_0}(m_0) \Rightarrow \forall j_1\ AB\_deliver_{j_1} -\] - -Proof: -\begin{align*} - &\forall j_0, m_0\ AB\_deliver_{j_0}(m_0) \Rightarrow \exists j_1 \text{ correct }, AB\_broadcast(m_0) \\ - &\exists j_0, m_0 \quad AB\_broadcast_{j_0}(m_0) \Rightarrow \forall j_1,\ AB\_deliver_{j_1}(m_0) -\end{align*} \ No newline at end of file