0000226: lazy.read_if_val unsound

View Issue Details [ Jump to Notes ]

Project

Tags

No tags attached.

Attached Files

Relationships

Relationships

Notes
~0000377 pbone (administrator) 2011-11-03 11:25	I presume you mean that it is unsound in the sense that it could be re-ordered with respect to force and have a different result. For example. Y = force(L), read_if_val(L, X) will succeed, but read_if_val(L, X), Y = force(L) will not. I agree that this might be a problem but I can't see the problem ever arising. force is pure because the internal state of the lazy value has no effect on any other part of the system (other than read_if_val). read_if_val is pure (and force is pure) because I haven't seen a real-life case where the ordering of force and read_if_val matters. I've only used read_if_val once (the deep profiler feedback tool's pretty printer). And in that case the corresponding call to force was in a separate peice of code, and I do not want to have to propagate the impurity throughout all that code to enforce the ordering of force and read_if_val, so making these non-pure would not be useful. If anyone can show a non-contrived case where the ordering of these calls is important and should be enforced using the purity system then I'd be happy to reconsider.

~0000381 wangp (developer) 2011-11-03 12:37	Paul, the predicate build_var_use_list(Map, Var, !List) may produce different output for the same input.

~0000382 pbone (administrator) 2011-11-03 15:39	That doesn't matter, build_var_use is only called after the analysis has finished, and we're going to write the output into the feedback file. Or from a trace goal. It is used to prevent us from forcing the evaluation of results that aren't actually used in the analysis, and only include those that are used in the feedback report or output of trace goals

~0000383 wangp (developer) 2011-11-03 17:37	The point is that it could be any predicate since lazy values could be embedded anywhere. The existence of read_if_val breaks referential transparency.

~0000384 juliensf (administrator) 2011-11-04 00:27	I agree, read_if_val/2 should be made semipure.

~0000386 zs (developer) 2011-11-04 00:52	I also agree. However, please don't make it semipure just yet. I have an incomplete diff that I expect will remove some uses of read_if_val from the deep profiler directory, and I would like to avoid conflicts.

~0000387 pbone (administrator) 2011-11-04 11:16	Okay, My remaining concern is that a semipure read_if_val only makes sense if force is impure. However when a programmer never uses read_if_val they still have to work with an impure force. If read_if_val didn't exist, then force can be pure, because the impurity can never affect anything. Is there a better way to manage this, and still allow read_if_val to exist? Thanks.

~0000388 juliensf (administrator) 2011-11-04 12:38	I don't follow you: force is (and can remain) pure whatever the purity of read_if_val is.

~0000389 colanderman (reporter) 2011-11-04 12:52	Julien: I think you're right, a semipure read_if_val suffices. I think I was understanding impurity backward.

~0000390 pbone (administrator) 2011-11-04 13:26	read_if_val doesn't update any memory, so at best it's pure and at worst it's impure. force updates memory, so at worst it is impure, but it has a pure interface. read_if_val has an impure interface, since calls to force can cause it to not have referential transperency. My understanding of impurity is: + that pure gaols are allowed to be placed in any order with respect to one another, and even be optimized away. + that semipure goals are allowed to be placed in any order with respect to one another, and in any order with respect to pure goals, since none of these goals are side-affecting. (but semipure goals are affected by side effects). And that semipure goals can be optimized away. + that impure goals must be placed in order with respect to other impure and semipure goals. Since they are both side-effecting and side-effected. They may not be optimized away since their side effects may be deliberate. Please correct me if I am wrong. Therefore if read_if_val is semipure and force is pure, different orderings such as: read_if_val(L, X), Y = force(L) and Y = force(L), read_if_val(L, X) are considered equivalent (because the semipure and pure goals may be re-ordered) except that the former may fail and the latter will always succeed. To prevent this re-ordering, force needs to be marked as impure, so that it's side effect is recognized by the compiler, preventing the compiler from re-ordering these goals. Again, please correct me if I am mistaken.

~0000391 juliensf (administrator) 2011-11-04 13:39	Ok, you will need to use impurity to prevent the compiler (potentially ) reordering code there. I'm not quite sure how you concluded that it is force/1 should be impure though -- the non-referentially transparent procedure is read_if_val, so declare that to be impure (rather than semipure).

~0000392 pbone (administrator) 2011-11-04 13:55	Because force is the function that has a side-effect. read_if_val does not have a side-effect. If force is pure and read_if_val is impure then the compiler will think that it can re-order the two calls, pure and impure calls can be placed in any order. See my points about impurity above.

~0000393 juliensf (administrator) 2011-11-04 14:09	From the reference manual, section 15.3 Semantics [of purity levels] "Impure goals may not be reordered relative to any other goals; not even “minimal” reordering as implied by the modes is permitted." If the compiler does reorder the first goal in the following over the second then that is a bug in the compiler. Y = force(L), impure read_if_val(L, X) Making force impure is (1) unnecessary and (2) misses the entire point of the lazy module which is to provide a _pure interface_ to lazy evaluation. (It is read_if_val/2 that subverts this pure interface, it is the source of the non-purity here.)

~0000394 pbone (administrator) 2011-11-04 14:22	Okay, I didn't realize that impurity was that strong. Yes, this is also why I wanted to avoid making force impure, since it and delay provide the pure interface. I find this unintuitive WRT where the side-effects are.

~0000493 juliensf (administrator) 2013-01-08 12:33	Fixed.

Notes

Date Modified	Username	Field	Change
Issue History
2011-11-03 10:21	colanderman	New Issue
2011-11-03 11:25	pbone	Note Added: 0000377
2011-11-03 12:37	wangp	Note Added: 0000381
2011-11-03 15:39	pbone	Note Added: 0000382
2011-11-03 17:37	wangp	Note Added: 0000383
2011-11-04 00:27	juliensf	Note Added: 0000384
2011-11-04 00:52	zs	Note Added: 0000386
2011-11-04 11:16	pbone	Note Added: 0000387
2011-11-04 11:17	pbone	Status	new => assigned
2011-11-04 11:17	pbone	Assigned To	=> pbone
2011-11-04 12:38	juliensf	Note Added: 0000388
2011-11-04 12:52	colanderman	Note Added: 0000389
2011-11-04 13:26	pbone	Note Added: 0000390
2011-11-04 13:39	juliensf	Note Added: 0000391
2011-11-04 13:55	pbone	Note Added: 0000392
2011-11-04 14:09	juliensf	Note Added: 0000393
2011-11-04 14:22	pbone	Note Added: 0000394
2013-01-08 12:33	juliensf	Note Added: 0000493
2013-01-08 12:33	juliensf	Status	assigned => resolved
2013-01-08 12:33	juliensf	Resolution	open => fixed
2013-01-08 12:33	juliensf	Assigned To	pbone => juliensf

Issue History