Skip to content
Snippets Groups Projects
Commit 2004bc68 authored by Justin Loew's avatar Justin Loew
Browse files

Move paper to a git submodule on Overleaf

parent 0762166e
No related branches found
No related tags found
No related merge requests found
[submodule "Paper"]
path = Paper
url = https://git.overleaf.com/15360786jksgwrrzdqyf
Paper @ 8349afc5
Subproject commit 8349afc5786f1b98041088bc0431312bd2f143c7
*.aux
*.bbl
*.blg
*.log
*.out
*.synctex.gz
*.synctex(busy)
*.pdf
\def\filedate{2006/05/16}
\def\fileversion{1.02}
\ProvidesPackage{AMMALanguages}
[\filedate\space\fileversion\space(Davide Di Ruscio and Frédéric Jouault)]
\typeout{}
\typeout{----------------------}
\typeout{AMMA Languages Formatting Package}
\typeout{----------------------}
\typeout{}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\usepackage{listings}
\usepackage{color}
%\usepackage{xspace}
%\usepackage{amsmath}
\definecolor{gray}{rgb}{0.94,0.94,0.94}
\definecolor{blue}{rgb}{0,0,0.5}
%\lstloadlanguages{HTML,XML}
\lstset{
% backgroundcolor=\color{gray},
breaklines=true,
frame=single,
framerule=0pt,
language=,
numbers=left,
numbersep=5pt,
showspaces=false,
showtabs=false,
tabsize=4,
basicstyle=\ttfamily\scriptsize,
%basicstyle=\scriptsize,
commentstyle=\ttfamily\itshape\bfseries,
identifierstyle=\ttfamily\scriptsize,
%\bfseries,
numberstyle=\ttfamily\tiny
}
\definecolor{keywordColor}{rgb}{.5, 0, .33}
%\definecolor{keywordColor}{rgb}{0, 0, 0}
\definecolor{commentColor}{rgb}{0, .3, 0}
\definecolor{backgroundColor}{rgb}{.9, .9, .9}
\definecolor{emphColor}{rgb}{.16, 0, 1}
\definecolor{numberColor}{rgb}{.09, .62, .28}
%[breaklines,mathescape,rulesepcolor=\color{black}]
\lstdefinestyle{AMMA}{
backgroundcolor=\color{backgroundColor},
basicstyle=\scriptsize,
% keywordstyle=\color{[rgb]{.5, 0, .33}}\bfseries,
keywordstyle=\color{keywordColor}\bfseries,
stringstyle=\color{blue}\ttfamily,
% commentstyle=\color{[rgb]{0, 0.5, 0}}\ttfamily,
commentstyle=\color{commentColor}\ttfamily,
emphstyle=\color{emphColor},
% numberstyle=\color{numberColor},
tabsize=2,
frame=,
breaklines=true,
% postbreak={(*@$\hookrightarrow$@*)},
% postbreak={(*@$\nearrow$@*)},
% postbreak=\mbox{{\color{red}\tiny$\rightarrow$}},
postbreak=\mbox{{\color{red}\tiny$\hookrightarrow$}},
}
\lstdefinelanguage{TCS}{
morekeywords={main,template,isDefined,addToContext,primitiveTemplate,for,default,using,context},
morekeywords={operators,priority,operatorTemplate,source,storeOpTo,storeRightTo},
morekeywords={symbols,leftSpace,rightSpace,leftNone,rightNone},
morekeywords={nbNL,indentIncr},
morekeywords={as,refersTo,separator},
sensitive=true,
morecomment=[l]{--},
morestring=[b]",
}
\lstdefinelanguage{KM3}{
morekeywords={package,class,oppositeOf,container,ordered,abstract,extends,reference,attribute,enumeration,literal,datatype},
emph={Boolean,Integer,String},
sensitive=true,
morecomment=[l]{--},
morestring=[b]",
}
\lstdefinelanguage{ATL}{
morekeywords={rule,module,from,to,create,uses, using, do, helper, def},
emph={Boolean,Integer,String,Sequence},
sensitive=true,
morecomment=[l]{--},
morestring=[b]',
}
\lstdefinelanguage{ANTLR}{
morekeywords={},
% we use emph for (some) terminals
emph={LCURLY,RCURLY,NAME},
sensitive=true,
morecomment=[l]{//},
morestring=[b]",
}
\lstdefinelanguage{SPL}{
morekeywords={service,processing,registration,return,forward,incoming},
emph={uri,response},
sensitive=true,
morecomment=[l]{//},
morestring=[b]',
}
\lstdefinelanguage{XASM}{
morekeywords={asm,endasm,is,choose,in,do,forall,and,or,then,endchoose,enddo,if,endif,then,universes,universe,function,
exists,not,extend,endextend},
emph={Boolean,Integer,String,Sequence},
sensitive=true,
morecomment=[l]{--},
morestring=[b]',
}
\lstdefinelanguage{ASP}{
morekeywords={node, prop, edge, not, relation, nodet, edget, propt, metanode, metaprop, metaedge},
sensitive=true,
morecomment=[l]{//},
morestring=[b]',
}
\lstdefinelanguage{Maude}{
morekeywords={fmod, endfm, mod, omod, tmod, endm, endom, endtm, is, pr, protecting, crl, rl},
morekeywords={op, ops, eq, ceq, sort, sorts, class, subsort, subsorts, subclass, subclasses, vars, var, if},
morekeywords={Maude, result, cmb},
sensitive=true,
morecomment=[l]{---},
morestring=[b]",
}
\lstdefinelanguage{OCL20}{
morekeywords={context, inv, body},
emph={Boolean,Integer,String,Sequence, Bag, self, Set},
sensitive=true,
morecomment=[l]{--},
morestring=[b]',
}
\endinput
@article{lamport:bakery,
AUTHOR = "Leslie Lamport",
TITLE = "A New Solution of Dijkstra's Concurrent Programming Problem",
JOURNAL = "Communications of the ACM",
YEAR = "1974",
VOLUME = "17",
NUMBER = "8",
PAGES = "453--455",
}
@article{lamport:multi-reader-single-writer,
AUTHOR = "Leslie Lamport",
TITLE = "Concurrent Reading and Writing",
JOURNAL = "Communications of the ACM",
YEAR = 1977,
VOLUME = 20,
NUMBER = 11,
PAGES = "806--811",
}
@article{lamport:lamport-timestamps,
AUTHOR = "Leslie Lamport",
TITLE = "Time, Clocks, and the Ordering of Events in a Distributed System",
JOURNAL = "Communications of the ACM",
YEAR = 1978,
VOLUME = 21,
NUMBER = 7,
PAGES = "558--565",
}
@article{lamport:proving-concurrent-programs,
AUTHOR = "Leslie Lamport",
TITLE = "A New Approach to Proving the Correctness of Multiprocess Programs",
JOURNAL = "ACM Transactions on Programming Languages and Systems",
YEAR = 1979,
VOLUME = 1,
NUMBER = 1,
PAGES = "84--97",
}
@article{lamport:interprocess-communication,
AUTHOR = "Leslie Lamport",
TITLE = "On Interprocess Communication",
JOURNAL = "Distributed Computing",
YEAR = 1985,
VOLUME = 1,
NUMBER = 2,
PAGES = "77--101",
}
@report{impossibility-of-consensus,
AUTHOR = "Michael J. Fischer, Nancy A. Lynch and Michael S. Paterson",
TITLE = "Impossibility of Distributed Consensus with One Faulty Process",
YEAR = 1982,
NUMBER = 245,
}
@Inbook{Sedletsky2000,
author="Sedletsky, Ekaterina
and Pnueli, Amir
and Ben-Ari, Mordechai",
editor="Kapoor, Sanjiv
and Prasad, Sanjiva",
title="Formal Verification of the Ricart-Agrawala Algorithm",
bookTitle="FST TCS 2000: Foundations of Software Technology and Theoretical Computer Science: 20th Conference New Delhi, India, December 13--15, 2000 Proceedings",
year="2000",
publisher="Springer Berlin Heidelberg",
address="Berlin, Heidelberg",
pages="325--335",
abstract="This paper presents the first formal verification of the Ricart- Agrawala algorithm [RA81] for distributed mutual exclusion of an arbitrary number of nodes. It uses the Temporal Methodology of [MP95a]. We establish both the safety property of mutual exclusion and the liveness property of accessibility. To establish these properties for an arbitrary number of nodes, parameterized proof rules are used as presented in [MP95a] (for safety) and [MP94] (for liveness). A new and efficient notation is introduced to facilitate the presentation of liveness proofs by verification diagrams.",
isbn="978-3-540-44450-3",
doi="10.1007/3-540-44450-5_26",
url="https://doi.org/10.1007/3-540-44450-5_26"
}
@article{ricart-agrawala,
author = {Ricart, Glenn and Agrawala, Ashok K.},
title = {An Optimal Algorithm for Mutual Exclusion in Computer Networks},
journal = {Commun. ACM},
issue_date = {Jan. 1981},
volume = {24},
number = {1},
month = jan,
year = {1981},
issn = {0001-0782},
pages = {9--17},
numpages = {9},
url = {http://doi.acm.org/10.1145/358527.358537},
doi = {10.1145/358527.358537},
acmid = {358537},
publisher = {ACM},
address = {New York, NY, USA},
keywords = {concurrent programming, critical section, distributed algorithm, mutual exclusion, network, synchronization},
}
@InCollection{kshemkalyani-singhal,
author = {Kshemkalyani, Ajay and Singhal, Mukesh},
title = {Distributed Mutual Exclusion Algorithms},
booktitle = {Distributed Computing: Principles, Algorithms, and Systems},
chapter = 9,
publisher = {Cambridge University Press},
year = 2008,
url = {https://www.cs.uic.edu/~ajayk/Chapter9.pdf},
}
This diff is collapsed.
This diff is collapsed.
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment