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

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

logo moved

File size: 12.4 KB
8\vspace*{1cm}Project FP7-ICT-2009-C-243881 \cerco{}}
10\date{ }
30Report n. D6.1\\
31Project Web Site and Software Repository\\
38Version 1.0
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\clearpage \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\cite{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~\cite{trac}) 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 based on the \emph{unstable} version
116   of the Debian distribution and it is configured with all the libraries
117   required by Matita and the OCaml ones we plan to use for CerCo .
120The Department of Computer Science of the University of Bologna also provides
121an archived mailing list dedicated to the project members for general
122discussions and coordination. The archives are private and accessible to
123project members only.
125To maximise fault tolerance, we configured the server with RAID 5, so that
126the loss of one hard disk does not compromise the data. Moreover, we provide
127incremental nightly backups of all the sensible data and we store the backups
128on a different physical machine. The main motivation is to be able to recover
129accidentally deleted files or old machine configurations.
131Finally, the \cerco{} server acts as a network file system, NIS and DNS server for
132a cluster of virtual and physical machines (at the moment all located in
133Bologna) that can also be used for \cerco{} development.
135We discuss now the implementation of the ``Web Site'', Software Repository and
136Continuous Building System.
138\section{Project ``Web Site'' (Trac)}\label{site}
139In order to ease the creation of a community around the \cerco{} prototype, it
140was decided to prefer a Wiki-centred solution to a traditional Web Site.
141Our choice has been to install a personalised version of the
142Integrated SCM \& Project Management tool Trac~\cite{trac}, accessible at
144Trac provides in an integrated and lightweight solution:
145 \begin{enumerate}
146  \item A Wiki for the advertisement and dissemination of the project results,
147    and for fostering discussions and contributions from the user community.
148  \item An issue tracking system that subsumes a bug tracking system and
149    provides a basic control over the project advancement.
150  \item An on-line, simplified Web interface to the software repository.
151  \item A flexible system of plug-ins to add new functionalities or modify
152    the behaviour of the basic ones.
153 \end{enumerate}
154By means of additional plug-ins, we have integrated the public part of the
155Wiki with a private one. The private part is meant to integrate the mailing
156list in facilitating the discussion between the project developers. Moreover,
157since it is integrated with the software repository and Issue tracking systems,
158it is possible to create hyper-links to or to embed in discussion pages
159both code fragments and description of issues.
161\section{Software Repository}\label{repo}
162After considering several alternatives, it was decided to use a centralised
163software repository for the \cerco{} project, and we installed Subversion~\cite{subversion} on the
164\cerco{} server. Project members that prefer a distributed solution or that are
165used to work without network connectivity are advised to use the svn-git
166software to mirror the centralised repository.
168The repository is open in read mode to anonymous users, and in write mode to
169project members only. A simplified web interface to the repository is also
170integrated in Trac and publicly available.
172\section{Continuous Building System}\label{cbs}
173In \cerco{} we will develop both certified code (in Matita) and standard one
174(mainly in OCaml). We plan to adopt traditional testing methods (e.g. unit
175testing) to control bug regressions in the standard code, while the certified
176code will be checked by asking Matita to verify all the definitions and proofs
177of correctness. The last operation in particular can require quite a lot of
178time (in the order of at most a few hours), especially if proof automation will
179be heavily used in Matita to reduce the proving effort. Moreover, as already
180explained, we expect to observe a continuous evolution of Matita (and its
181standard library) to parallel the development of the \cerco. Each change in
182the code of Matita must trigger not only the checking for regressions on the
183\cerco{} code, but also on all the existent developments made in Matita (in order
184to avoid the possibility of introducing a bug that jeopardise the whole
185project or that will later require other changes before the next official
186release of Matita).
188Since re-checking all the Matita developments already
189requires several hours even on a fast machine, we cannot expect the developers
190of \cerco{} to delay distribution of their changes to the partners until all the
191regression tests have been performed. Moreover, it is fundamental to keep trace
192of the evolution of the performances of both the code of Matita and the code of
193the \cerco{} prototype. Performance checks are meaningful only if systematically
194repeated always on the same machine and with reproducible load conditions.
195Hence we put up an ad-hoc continuous building system for Matita+\cerco{} that
196supports the following workflow:
198 \item Commits are always allowed and developers are invited to commit as soon
199   as they obtain a code that compiles and seems to implement the wanted
200   changes on ad-hoc tests. When the commit is supposed to close a bug, the
201   developer is also requested to commit a test for the bug to avoid future
202   regressions. Development branches are encouraged on personal copies of the
203   repository (using git-svn), but are discouraged on the central repository.
204 \item Every night the CBS virtual machine is brought back to a pristine
205   condition and a script checks-out the latest version of the Matita and \cerco{}
206   code, compiles the code of Matita, verifies the standard library, all
207   the contribs of Matita and the certified \cerco{} code, and run all the
208   regression tests on both the certified and un-certified code. All faults
209   are recorded, as well as the performance of Matita on each source file.
210 \item The statistics collected every night are stored in a data-base (a
211   mysql instance) that runs on the virtual machine. The
212   Subversion revision number is associated to the results in the statistics.
213   Another set of scripts compares the statistics with those collected the
214   previous
215   night and, in case of significant regressions, sends a notification to all
216   developers (using the \cerco{} mailing list).
217 \item The developers can consult an ad-hoc web-interface to the data-base
218   (written in python) that implements a set of ad-hoc queries or that allows
219   the user to submit his own (by writing SQL code). In particular,
220   the following predefined queries are available among others:
221   \begin{enumerate}
222    \item Showing the list of commits between two given dates. In particular,
223     the user can discover who is responsible for a commit that
224     introduced a regression or that had a negative impact on performances.
225    \item Compare the statistics between two dates or revision numbers.
226    \item Monitor the performance evolution of the system on a single test.
227   \end{enumerate}
230On purpose, the CBS does not retract the commits that introduce regressions.
231We expect that the developers that are responsible for regressions will
232retract their code the very next day, or they will fix the regression or they
233will notify the other developers on the reasons for not fixing the regression
234(e.g. when the regression is actually caused by an already present bug that
235was previously masked by some other fault).
237\section{Future evolutions}
239The software architecture implemented so far is fully sufficient to support the
240initial development of \cerco. Moreover, the public part of the Wiki has been
241loaded with an overall description of the project that was largely obtained by
242the grant agreement. We expect the system to keep evolving during the lifetime
243of \cerco{} both in the public (and private) contents and in the code of the
244continuous building system. We will also consider in the future the opportunity
245of integrating other services in the Trac interface, like live demos of the
246\cerco{} prototype.
249\bibitem{matita} The Interactive Theorem Prover Matita,
250 \url{}
251\bibitem{subversion}The Version Control System Subversion,
252 \url{}
253\bibitem{trac}The Integrated SCM \& Project Management tool Trac,
254 \url{}
Note: See TracBrowser for help on using the repository browser.