source: Deliverables/D6.1/report.tex @ 7

Last change on this file since 7 was 7, checked in by sacerdot, 11 years ago


File size: 12.2 KB
2%\usepackage[a4paper=true,  bookmarks=true, linkcolor=black, citecolor=black, urlcolor=black,colorlinks=true,pagecolor=black, breaklinks=true, bookmarksopen=true]{hyperref}
3\usepackage{latexsym, amssymb, amsfonts}
16\vspace*{1cm}Project FP7-ICT-2009-C-243881 \cerco{}}
18\date{ }
37Report n. D6.1\\
38Project Wet Site and Software Repository
45Main Authors:\\
46M Puech, C. Sacerdoti Coen
52Project Acronym: \cerco{}\\
53Project full title: Certified Complexity\\
54Proposal/Contract no.: FP7-ICT-2009-C-243881 \cerco{}\\
56\newpage \pagestyle{myheadings} \markright{\cerco{}, FP7-ICT-2009-C-243881}
61The deliverable D6.1 \emph{Project Web Site and Software Repository} is the
62first \textbf{prototype} of the \cerco{} project. The deliverable is
63\textbf{public}, although part of the data handled by it are private, and
64required an effort of about \textbf{3 person-months}.
65The description of the deliverable in the Grant Agreement is the following one:
67A web site will be designed and realised, and each partner will
68contribute to its content. The site will comprise a public part, accessible to everyone, and a private one, reserved
69to the project partners for the exchange of documentation, material, and to support project related activities. We
70will also install a revision control system (like SVN or GIT) to keep track of software evolution and we will adapt
71an existent continuous building system to trace software regressions nightly, in batch mode.
75The aim of D6.1 is twofold: it must provide the main
76technological infrastructure for the advertisement and dissemination of the
77research results of \cerco{}, and it must also provide the means for direct
78communication and resource sharing among partners. Moreover, UNIBO will provide
79to the other partners the Matita interactive theorem prover that will be used
80to obtain the certified \cerco{} compiler. We expect to make Matita evolve during
81the project timeframe in order to fix bugs that are critical for \cerco{} and in
82order to implement ad-hoc features. It is fundamental to grant to our
83partners immediate access to the changes of Matita and to monitor the
84behaviour of the system on the \cerco{} sources to avoid regressions and bugs
85introduction. Therefore, we plan to achieve a strict integration between
86the technological infrastructure for the development of Matita and the one for
89In order to target the previous
90objectives, UNIBO (the project coordinator) has bought a server to be dedicated
91to the project with the following characteristics:
93Dell PowerEdge R410, 16GB Memory for 1 CPU, DDR3, 1333MHz, Intel Xeon X5570, 2.93Ghz, 8M Cache, 4 x 300 GB, 15K RPM Hard Drive (HOT SWAP), RAID controller.
96The server characteristics have been chosen to allow for multiple virtual
97machines. In particular, for safety and flexibility purposes, direct access to
98the server is not allowed, but the server currently exposes the following
99virtual machines that can be accessed from the outside:
101 \item[] This virtual machine hosts the ``project web site''
102   (actually, a Trac instance) and
103   the software repository. These services are discussed in
104   Sections~\ref{site} and~\ref{repo}. We installed on it the \emph{stable}
105   version of the Debian distribution of Linux in order to maximise
106   availability.
107 \item[] This virtual machine hosts the continuous building
108   system (CBS) for Matita and \cerco{} that is discusses in Section~\ref{cbs}.
109   We installed on it the \emph{unstable} version of the Debian distribution
110   in order to immediately exploit the most recent developments of the software
111   library that will be used in \cerco{}.
112 \item[] This is the development virtual machine of
113   \cerco{}. It is open to all project participants in order to do remote
114   development and testing in a controlled environment that has all the
115   required libraries and tools. It is also base on the \emph{unstable} version
116   of the Debian distribution.
119The Department of Computer Science of the University of Bologna also provides
120an archived mailing list dedicated to the project members for general
121discussions and coordination. The archives are private and accessible to
122project members only.
124To maximise fault tolerance, we configured the server with RAID 5, so that
125the loss of one hard disk does not compromise the data. Moreover, we provide
126incremental nightly backups of all the sensible data and we store the backups
127on a different physical machine. The main motivation is to be able to recover
128accidentally deleted files or old machine configurations.
130Finally, the \cerco{} server acts as a network file system, NIS and DNS server for
131a cluster of virtual and physical machines (at the moment all located in
132Bologna) that can also be used for \cerco{} development.
134We discuss now the implementation of the ``Web Site'', Software Repository and
135Continuous Building System.
137\section{Project ``Web Site'' (Trac)}\label{site}
138In order to ease the creation of a community around the \cerco{} prototype, it
139was decided to prefer a Wiki-centred solution to a traditional Web Site.
140Our choice has been to install a personalised version of the
141Integrated SCM \& Project Management tool Trac (
142Trac provides in an integrated and lightweight solution:
143 \begin{enumerate}
144  \item A Wiki for the advertisement and dissemination of the project results,
145    and for fostering discussions and contributions from the user community.
146  \item An issue tracking system that subsumes a bug tracking system and
147    provides a basic control over the project advancement.
148  \item An on-line, simplified Web interface to the software repository.
149  \item A flexible system of plug-ins to add new functionalities or modify
150    the behaviour of the basic ones.
151 \end{enumerate}
152By means of additional plug-ins, we have integrated the public part of the
153Wiki with a private one. The private part is meant to integrate the mailing
154list in facilitating the discussion between the project developers. Moreover,
155since it is integrated with the software repository and Issue tracking systems,
156it is possible to create hyper-links to or to embed in discussion pages
157both code fragments and description of issues.
159\section{Software Repository}\label{repo}
160After considering several alternatives, it was decided to use a centralised
161software repository for the \cerco{} project, and we installed Subversion on the
162\cerco{} server. Project members that prefer a distributed solution or that are
163used to work without network connectivity are advised to use the svn-git
164software to mirror the centralised repository.
166The repository is open in read mode to anonymous users, and in write mode to
167project members only. A simplified web interface to the repository is also
168integrated in Trac and publicly available.
170\section{Continuous Building System}\label{cbs}
171In \cerco{} we will develop both certified code (in Matita) and standard one
172(mainly in OCaml). We plan to adopt traditional testing methods (e.g. unit
173testing) to control bug regressions in the standard code, while the certified
174code will be checked by asking Matita to verify all the definitions and proofs
175of correctness. The last operation in particular can require quite a lot of
176time (in the order of at most a few hours), especially if proof automation will
177be heavily used in Matita to reduce the proving effort. Moreover, as already
178explained, we expect to observe a continuous evolution of Matita (and its
179standard library) to parallel the development of the \cerco{}. Each change in
180the code of Matita must trigger not only the checking for regressions on the
181\cerco{} code, but also on all the existent developments made in Matita (in order
182to avoid the possibility of introducing a bug that jeopardise the whole
183project or that will later require other changes before the next official
184release of Matita).
186Since re-checking all the Matita developments already
187requires several hours even on a fast machine, we cannot expect the developers
188of \cerco{} to delay distribution of their changes to the partners until all the
189regression tests have been performed. Moreover, it is fundamental to keep trace
190of the evolution of the performances of both the code of Matita and the code of
191the \cerco{} prototype. Performance checks are meaningful only if systematically
192repeated always on the same machine and with reproducible load conditions.
193Hence we put up an ad-hoc continuous building system for Matita+CerCo that
194supports the following workflow:
196 \item Commits are always allowed and developers are invited to commit as soon
197   as they obtain a code that compiles and seems to implement the wanted
198   changes on ad-hoc tests. When the commit is supposed to close a bug, the
199   developer is also requested to commit a test for the bug to avoid future
200   regressions. Development branches are encouraged on personal copies of the
201   repository (using git-svn), but are discouraged on the central repository.
202 \item Every night the CBS virtual machine is brought back to a pristine
203   condition and a script checks-out the latest version of the Matita and CerCo
204   code, compiles the code of Matita, verifies the standard library, all
205   the contribs of Matita and the certified CerCo code, and run all the
206   regression tests on both the certified and un-certified code. All faults
207   are recorded, as well as the performance of Matita on each source file.
208 \item The statistics collected every night are stored in a data-base (a
209   mysql instance) that runs on the virtual machine. The
210   Subversion revision number is associated to the results in the statistics.
211   Another set of scripts compares the statistics with those collected the
212   previous
213   night and, in case of significant regressions, sends a notification to all
214   developers (using the \cerco{} mailing list).
215 \item The developers can consult an ad-hoc web-interface to the data-base
216   (written in python) that implements a set of ad-hoc queries or that allows
217   the user to submit his own (by writing SQL code). In particular,
218   the following predefined queries are available among others:
219   \begin{enumerate}
220    \item Showing the list of commits between two given dates. In particular,
221     the user can discover who is responsible for a commit that
222     introduced a regression or that had a negative impact on performances.
223    \item Compare the statistics between two dates or revision numbers.
224    \item Monitor the performance evolution of the system on a single test.
225   \end{enumerate}
228On purpose, the CBS does not retract the commits that introduce regressions.
229We expect that the developers that are responsible for regressions will
230retract their code the very next day, or they will fix the regression or they
231will notify the other developers on the reasons for not fixing the regression
232(e.g. when the regression is actually caused by an already present bug that
233was previously masked by some other fault).
235\section{Future evolutions}
237The software architecture implemented so far is fully sufficient to support the
238initial development of \cerco. Moreover, the public part of the Wiki has been
239loaded with an overall description of the project that was largely obtained by
240the grant agreement. We expect the system to keep evolving during the lifetime
241of \cerco{} both in the public (and private) contents and in the code of the
242continuous building system. We will also consider in the future the opportunity
243of integrating other services in the Trac interface, like live demos of the
244\cerco{} prototype.
Note: See TracBrowser for help on using the repository browser.