SSG - A Parallel Refinement Checker
SSG is a tool to check the correctness of programs. You can check the correctness of large-scale programs in parallel by utilizing multicore CPUs and cloud power. SSG strongly supports the development of high-quality software by detecting problems which might be overlooked with tests.
What can SSG check?
SSG can check whether the implementation you are designing satisfies the specification or not. In addition, SSG can detect deadlocks and livelocks.
SSG compares the specification and the implementation, and generates the result report. If the implementation does not satisfy the specification, SSG records the trace from the initial state to the violating state in the report.
How to use SSG?
The process to check the correctness by SSG consists of several steps:
- Invoke SSG with a model file which includes the description of the specification and the implementation, and the assertions to be checked. SSG will convert them into a checking program in C.
- Compile the source file by gcc and link with libssg, and you will get the executable file.
- Run the executable file. It will check the correctnes and generate a report file. Note that the executable can run on other platforms such as PC with many cores and virtual machines on clouds.
Multicores and Cloud Power
SSG checks the correctness in parallel by using multicores. SSG has a worksteal engine which effectively maps the checking works to workers and balances the load of them.
The following graph shows a result of checking the safety of readers-writers problem. It was measured on an Intel XEON processor which has 32 cores (64 hyper-threads). As you can see, the speed of checking linearly scales up to 32 cores. (Note that it is said that the performance of hyper-thread is around 10~30%, which is the reason the curve is bent at 32 cores.)
||Linux, macOS, Microsoft Windows 10[*1] [*2]|
||Intel or AMD, x86_64 compatible CPU|
||4Gbytes or more[*3]|
||at least 100Mbytes availble space|
32bit operating systems are not supported.
Bash on Windows is requreied on Microsoft Windows 10.
The memory size needed to check depends on the size of target models to be checked.
SSG one license 97,200 JPY
- Please check the system requirements.
- Please read the End User License Agreement carefully. By purchasing the license of the software, you are agreeing to be bound by the terms of this license. If you do not agree to the terms of this license, do not purchase the license of the software.
- The payment can be done by PayPal only. If you are not familiar with PayPal, please visit https://www.paypal.com/.
- The product will be sent via e-mail normally within 3 working days
after the purchasing procedure.
SSG End User License Agreement
- (1)"PRINCIPIA" means PRINCIPIA Limited.
- (2)"Software" means the SSG executable file, the SSG library file, and all of the files delivered with the SSG files, including manuals and sample models.
- (3)"Customer" means an individual who purchased the license of the Software.
- Customer is permitted to use the Software provided that Customer agrees to all of the terms of this license. The Software is permitted to be used and not to be sold. PRINCIPIA keeps all rights of the Software except the rights which is explicitly permitted to Customer in this license.
- 3.Permitted License Uses
- Customer may use the Software on multiple computers provided that at most one instance of the execution of the program exists at any time.
- (1)Customer may not give, lend, sell the Software to a third party, and/or make the Software available over a network, except that the third party is also granted the license of the Software.
- (2)Customer may not modify and/or delete the copyright notice of the Software.
- 5.Disclaimer of Warranties
- (1)PRINCIPIA does not warrant that the Software has no defects, that the Software is error-free, and that the use of the Software does not give damage to a third party.
- (2)PRINCIPIA does not warrant to provide the corrected version of the Software if the Software is found to have defects.
- (3)To the extent not prohibited by applicable law, in no event shall PRINCIPIA be liable for any damage caused by the use of the Software. In no event shall PRINCIPIA's total liability to you for all damages exceed the price of one license.
- (1)PRINCIPIA may terminate the license if Customer violates the license.
- (2)Customer must cease all use of the Software and destroy all copies of the Software.
- 7.Personal Information
- (1)Customer allows PRINCIPIA to use the name and the e-mail
address of the Customer as the personal information provided that the
objectives of the use are to confirm the license and to notify emergency
information regarding serious defects of the Software. Customer allows
PRINCIPIA to send e-mails to the address of the Customer in order to confirm
the license and to notify emergency information.
- (2)Customer can requires PRINCIPIA to terminate using the
personal information. When Customer requires the termination of the use of
the personal information, PRINCIPIA will delete the personal
information. The license is in effect even if the personal information is
deleted. However, Customer may not re-register the personal information
and/or be granted upgrade services of the Software.
- (3)PRINCIPIA may refuse to accept that an individual is granted the license of the Software if the individual does not respond an e-mail sent to the registered address by PRINCIPIA.
- (4)When Customer requires PRINCIPIA to change the registered e-mail address, Customer must respond e-mails sent to both the old and new e-mail addresses in order to confirm that the request of the change is proper.
- (5)PRINCIPIA identifies the Customer by the following two
items: the name of the Customer which is granted to PRINCIPIA when the
Customer purchased the license and the e-mail address. PRINCIPIA may refuse
any claim from a person who does not have all of the these items.
- (6)Customer allows PRINCIPIA to send e-mails in order to
notify serious defects of the Software, and/or to notify that the
corrected version of the Software for the defects is available.
- (1)This license shall be governed by the laws of Japan.
- (2)The court with jurisdiction over the disputes related to the license shall be the Saitama District Court in Japan.
1 July, 2017