ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
cadical_random.cpp
Go to the documentation of this file.
1#include "global.h"
2
3#include "internal.hpp"
4
5/*------------------------------------------------------------------------*/
6
7// Our random number generator is seeded by default (i.e., in the default
8// constructor) with random seeds, which should be unique across machines,
9// processes and time. This makes this code below rather operating system
10// dependent. We also use in essence defensive programming, overlaying
11// several methods to get randomness since in the past we were bitten a
12// couple of times (and got the same seeds). Having several methods makes
13// it also simpler to port randomly initializing seeds to different
14// operating systems (even though currently it is only tested on Linux).
15// This functionality is only used in the 'Mobical' model based tester at
16// this point, since the main solver explicitly sets a random seed ('0' by
17// default in 'options.hpp') and also currently only uses this seed in the
18// local search procedure explicitly without using the default constructor.
19// It is crucial for 'Mobical' to make sure that concurrent runs are really
20// independent.
21
22/*------------------------------------------------------------------------*/
23
24// Uncomment the following definition to force printing the computed hash
25// values for individual machine and process properties. This is only needed
26// for testing, porting and debugging different ports of this seeding and
27// hashing functions (uncomment and run 'mobical' for instance).
28
29/*
30#define DO_PRINT_HASH
31*/
32
33#ifdef DO_PRINT_HASH
34#define PRINT_HASH(H) \
35 do { \
36 printf ("c PRINT_HASH %32s () = %020" PRIu64 "\n", __func__, H); \
37 fflush (stdout); \
38 } while (0)
39#else
40#define PRINT_HASH(...) \
41 do { \
42 } while (0)
43#endif
44
45/*------------------------------------------------------------------------*/
46
47// This is Linux specific but if '/var/lib/dbus/machine-id' does not exist
48// does not have any effect. TODO: add a similar machine identity hashing
49// function for other operating systems (Windows and macOS).
50
52
53namespace CaDiCaL {
54
55static uint64_t hash_machine_identifier () {
56 FILE *file = fopen ("/var/lib/dbus/machine-id", "r");
57 uint64_t res = 0;
58 if (file) {
59 char buffer[128];
60 memset (buffer, 0, sizeof buffer);
61 size_t bytes = fread (buffer, 1, sizeof buffer - 1, file);
62 CADICAL_assert (bytes);
63 fclose (file);
64 if (bytes && bytes < sizeof buffer) {
65 buffer[bytes] = 0;
66 res = hash_string (buffer);
67 }
68 }
69 PRINT_HASH (res);
70 return res;
71}
72
73} // namespace CaDiCaL
74
76
77/*------------------------------------------------------------------------*/
78
79// On our Linux cluster where we used an NFS mounted root disk the
80// 'machine-id' above (even on a locally mounted '/var' disk on each node)
81// was copied from '/etc/machine-id' which was shared among all nodes
82// (before figuring this out and fixing it). Thus the main idea of getting
83// different hash values through this machine identifier machines did not
84// work. As an additional measure to increase the possibility to get
85// different seeds we are now also using network addresses (explicitly).
86
87#ifndef WIN32
88
89extern "C" {
90#include <ifaddrs.h>
91#include <netdb.h>
92#include <netinet/in.h>
93#include <stdio.h>
94#include <stdlib.h>
95#include <sys/socket.h>
96}
97
98#endif
99
101
102namespace CaDiCaL {
103
104static uint64_t hash_network_addresses () {
105 uint64_t res = 0;
106
107 // We still need to properly port this to Windows, but since accessing the
108 // IP address is only required for better randomization during testing
109 // (running 'mobical' on a cluster for instance) it is not crucial unless
110 // you really need to run 'mobical' on a Windows cluster where each node
111 // has identical IP addresses.
112
113#ifndef WIN32
114 struct ifaddrs *addrs;
115 if (!getifaddrs (&addrs)) {
116 for (struct ifaddrs *addr = addrs; addr; addr = addr->ifa_next) {
117 if (!addr->ifa_addr)
118 continue;
119 const int family = addr->ifa_addr->sa_family;
120 if (family == AF_INET || family == AF_INET6) {
121 const int size = (family == AF_INET) ? sizeof (struct sockaddr_in)
122 : sizeof (struct sockaddr_in6);
123 char buffer[128];
124 if (!getnameinfo (addr->ifa_addr, size, buffer, sizeof buffer, 0, 0,
125 NI_NUMERICHOST)) {
126 uint64_t tmp = hash_string (buffer);
127#ifdef DO_PRINT_HASH
128 printf ("c PRINT_HASH %35s = %020" PRIu64 "\n", buffer, tmp);
129 fflush (stdout);
130#endif
131 res ^= tmp;
132 res *= 10000000000000000051ul;
133 }
134 }
135 }
136 freeifaddrs (addrs);
137 }
138#endif
139
140 PRINT_HASH (res);
141 return res;
142}
143
144} // namespace CaDiCaL
145
147
148/*------------------------------------------------------------------------*/
149
150// Hash the current wall-clock time in seconds.
151
152extern "C" {
153#include <time.h>
154}
155
157
158namespace CaDiCaL {
159
160static uint64_t hash_time () {
161 uint64_t res = ::time (0);
162 PRINT_HASH (res);
163 return res;
164}
165
166} // namespace CaDiCaL
167
169
170/*------------------------------------------------------------------------*/
171
172// Hash the process identified.
173
174extern "C" {
175#include <sys/types.h>
176#ifdef WIN32
177#include <process.h>
178#else
179#include <unistd.h>
180#endif
181}
182
184
185namespace CaDiCaL {
186
187static uint64_t hash_process () {
188 uint64_t res = getpid ();
189 PRINT_HASH (res);
190 return res;
191}
192
193} // namespace CaDiCaL
194
196
197/*------------------------------------------------------------------------*/
198
199// Hash the current number of clock cycles.
200
201#include <ctime>
202
204
205namespace CaDiCaL {
206
207static uint64_t hash_clock_cycles () {
208 uint64_t res = std::clock ();
209 PRINT_HASH (res);
210 return res;
211}
212
213} // namespace CaDiCaL
214
215/*------------------------------------------------------------------------*/
216
217namespace CaDiCaL {
218
219Random::Random () : state (1) {
220 add (hash_machine_identifier ());
221 add (hash_network_addresses ());
222 add (hash_clock_cycles ());
223 add (hash_process ());
224 add (hash_time ());
225#ifdef DO_PRINT_HASH
226 printf ("c PRINT_HASH %32s = %020" PRIu64 "\n", "combined", state);
227 fflush (stdout);
228#endif
229}
230
231} // namespace CaDiCaL
232
#define ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_END
#define CADICAL_assert(ignore)
Definition global.h:14
#define PRINT_HASH(...)
uint64_t hash_string(const char *str)
unsigned long long size
Definition giaNewBdd.h:39
Definition file.h:23
char * memset()